PairingObject-1 Show Code edit
thm (PairingObject-1 ((A z w)) () (∃ w (∀ z (↔ (∈ z w) (∨ (= z A) (= z y)))))
x A z EqualityBuilderLL
(→ (= x A) (↔ (= z x) (= z A)))
(= z y) buildDisjunctionRRInConsequent
(→ (= x A) (↔ (∨ (= z x) (= z y)) (∨ (= z A) (= z y))))
(∈ z w) buildBiconditionalLLInConsequent
(→ (= x A) (↔ (↔ (∈ z w) (∨ (= z x) (= z y))) (↔ (∈ z w) (∨ (= z A) (= z y)))))
z buildForAllInConsequent
(→ (= x A) (↔ (∀ z (↔ (∈ z w) (∨ (= z x) (= z y)))) (∀ z (↔ (∈ z w) (∨ (= z A) (= z y))))))
w buildThereExistsInConsequent
(→ (= x A) (↔ (∃ w (∀ z (↔ (∈ z w) (∨ (= z x) (= z y))))) (∃ w (∀ z (↔ (∈ z w) (∨ (= z A) (= z y)))))))
w z x y Pairing
(∃ w (∀ z (↔ (∈ z w) (∨ (= z x) (= z y)))))
VariableToObject
(∃ w (∀ z (↔ (∈ z w) (∨ (= z A) (= z y)))))
)
edit