ExtensionalityBiconditional Show Code edit
thm (ExtensionalityBiconditional ((A z) (B z)) ()
(↔ (= A B) (∀ z (↔ (∈ z A) (∈ z B))))
A B z MembershipBuilderLL
(→ (= A B) (↔ (∈ z A) (∈ z B)))
z addForAllToConsequent
(→ (= A B) (∀ z (↔ (∈ z A) (∈ z B))))
z A B Extensionality
(→ (∀ z (↔ (∈ z A) (∈ z B))) (= A B))
introduceBiconditionalFromImplications
(↔ (= A B) (∀ z (↔ (∈ z A) (∈ z B))))
)
edit