SingletonBuilder Show Code edit
thm (SingletonBuilder () () (→ (= A B) (= (singleton A) (singleton B)))
(= A B) ConjunctionIdempotence
(↔ (= A B) (∧ (= A B) (= A B)))
eliminateBiconditionalReverse
(→ (= A B) (∧ (= A B) (= A B)))
A B A B UnorderedPairBuilder
(→ (∧ (= A B) (= A B)) (= (unorderedPair A A) (unorderedPair B B)))
applySyllogism
(→ (= A B) (= (unorderedPair A A) (unorderedPair B B)))
A SingletonAsUnorderedPair
(= (singleton A) (unorderedPair A A))
B SingletonAsUnorderedPair
(= (singleton B) (unorderedPair B B))
buildEquality
(↔ (= (singleton A) (singleton B)) (= (unorderedPair A A) (unorderedPair B B)))
eliminateBiconditionalForward
(→ (= (unorderedPair A A) (unorderedPair B B)) (= (singleton A) (singleton B)))
applySyllogism
(→ (= A B) (= (singleton A) (singleton B)))
)
edit