Metamath Proof Explorer


Theorem en1eqsn

Description: A set with one element is a singleton. (Contributed by FL, 18-Aug-2008) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 4-Jan-2025)

Ref Expression
Assertion en1eqsn A B B 1 𝑜 B = A

Proof

Step Hyp Ref Expression
1 en1 B 1 𝑜 x B = x
2 eleq2 B = x A B A x
3 elsni A x A = x
4 3 sneqd A x A = x
5 2 4 syl6bi B = x A B A = x
6 5 imp B = x A B A = x
7 eqtr3 B = x A = x B = A
8 6 7 syldan B = x A B B = A
9 8 ex B = x A B B = A
10 9 exlimiv x B = x A B B = A
11 1 10 sylbi B 1 𝑜 A B B = A
12 11 impcom A B B 1 𝑜 B = A