Extensionality Show Code edit
thm (Extensionality ((A z) (B z)) ()
(→ (∀ z (↔ (∈ z A) (∈ z B))) (= A B))
# To prove this, we change <code>y</code> to <code>B</code>, using <code>VariableToObject</code> applied to <code>y = B → ((∀ z (z ∈ A ↔ z ∈ y) → A = y) ↔ (∀ z (z ∈ A ↔ z ∈ B) → A = B))</code>
y B z MembershipBuilderLL
(→ (= y B) (↔ (∈ z y) (∈ z B)))
(∈ z A) buildBiconditionalLLInConsequent
(→ (= y B) (↔ (↔ (∈ z A) (∈ z y)) (↔ (∈ z A) (∈ z B))))
z buildForAllInConsequent
(→ (= y B) (↔ (∀ z (↔ (∈ z A) (∈ z y))) (∀ z (↔ (∈ z A) (∈ z B)))))
y B A EqualityBuilderLL
(→ (= y B) (↔ (= A y) (= A B)))
buildImplicationInConsequent
(→ (= y B) (↔ (→ (∀ z (↔ (∈ z A) (∈ z y))) (= A y)) (→ (∀ z (↔ (∈ z A) (∈ z B))) (= A B))))
z A y Extensionality-1
(→ (∀ z (↔ (∈ z A) (∈ z y))) (= A y))
VariableToObject
(→ (∀ z (↔ (∈ z A) (∈ z B))) (= A B))
)
edit