UnorderedPairObject Show Code edit
thm (UnorderedPairObject ((A z) (B z)) ()
(↔ (∈ C (abstract z (∨ (= z A) (= z B)))) (∨ (= C A) (= C B)))
z y A B UnorderedPair-sub
(→ (= z y) (↔ (∨ (= z A) (= z B)) (∨ (= y A) (= y B))))
y C A B UnorderedPair-sub
(→ (= y C) (↔ (∨ (= y A) (= y B)) (∨ (= C A) (= C B))))
result y A B PairingObject
(∃ result (∀ y (↔ (∈ y result) (∨ (= y A) (= y B)))))
SetObject
(↔ (∈ C (abstract z (∨ (= z A) (= z B)))) (∨ (= C A) (= C B)))
)
edit