Extensionality-1 Show Code edit
# Extensionality—various corollaries and convenience theorems (easy consequences of
# the axiom).
thm (Extensionality-1 ((A z) ) () (→ (∀ z (↔ (∈ z A) (∈ z y))) (= A y))
# This lemma changes <code>x</code> to <code>A</code>, using <code>VariableToObject</code> applied to <code>x = A → ((∀ z (z ∈ x ↔ z ∈ y) → x = y) ↔ (∀ z (z ∈ A ↔ z ∈ y) → A = y))</code>
x A z MembershipBuilderLL
(→ (= x A) (↔ (∈ z x) (∈ z A)))
(∈ z y) buildBiconditionalRRInConsequent
(→ (= x A) (↔ (↔ (∈ z x) (∈ z y)) (↔ (∈ z A) (∈ z y))))
z buildForAllInConsequent
(→ (= x A) (↔ (∀ z (↔ (∈ z x) (∈ z y))) (∀ z (↔ (∈ z A) (∈ z y)))))
x A y EqualityBuilderRR
(→ (= x A) (↔ (= x y) (= A y)))
buildImplicationInConsequent
(→ (= x A) (↔ (→ (∀ z (↔ (∈ z x) (∈ z y))) (= x y)) (→ (∀ z (↔ (∈ z A) (∈ z y))) (= A y))))
z x y ExtensionalityVariable
(→ (∀ z (↔ (∈ z x) (∈ z y))) (= x y))
VariableToObject
(→ (∀ z (↔ (∈ z A) (∈ z y))) (= A y))
)
edit