Singleton Show Code edit
thm (Singleton () () (↔ (∈ B (singleton A)) (= B A))
A SingletonAsUnorderedPair
(= (singleton A) (unorderedPair A A))
B buildMembershipLL
(↔ (∈ B (singleton A)) (∈ B (unorderedPair A A)))
B A A UnorderedPair
(↔ (∈ B (unorderedPair A A)) (∨ (= B A) (= B A)))
applyBiconditionalTransitivity
(↔ (∈ B (singleton A)) (∨ (= B A) (= B A)))
(= B A) DisjunctionIdempotence
(↔ (= B A) (∨ (= B A) (= B A)))
swapBiconditional
(↔ (∨ (= B A) (= B A)) (= B A))
applyBiconditionalTransitivity
(↔ (∈ B (singleton A)) (= B A))
)
edit