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