Metamath Proof Explorer

Theorem en1eqsn

Description: A set with one element is a singleton. (Contributed by FL, 18-Aug-2008)

Ref Expression
Assertion en1eqsn 
|- ( ( A e. B /\ B ~~ 1o ) -> B = { A } )

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 ssid 
 |-  1o C_ 1o
3 ssnnfi 
 |-  ( ( 1o e. _om /\ 1o C_ 1o ) -> 1o e. Fin )
4 1 2 3 mp2an 
 |-  1o e. Fin
5 enfii 
 |-  ( ( 1o e. Fin /\ B ~~ 1o ) -> B e. Fin )
6 4 5 mpan 
 |-  ( B ~~ 1o -> B e. Fin )
7 6 adantl 
 |-  ( ( A e. B /\ B ~~ 1o ) -> B e. Fin )
8 snssi 
 |-  ( A e. B -> { A } C_ B )
9 8 adantr 
 |-  ( ( A e. B /\ B ~~ 1o ) -> { A } C_ B )
10 ensn1g 
 |-  ( A e. B -> { A } ~~ 1o )
11 ensym 
 |-  ( B ~~ 1o -> 1o ~~ B )
12 entr 
 |-  ( ( { A } ~~ 1o /\ 1o ~~ B ) -> { A } ~~ B )
13 10 11 12 syl2an 
 |-  ( ( A e. B /\ B ~~ 1o ) -> { A } ~~ B )
14 fisseneq 
 |-  ( ( B e. Fin /\ { A } C_ B /\ { A } ~~ B ) -> { A } = B )
15 7 9 13 14 syl3anc 
 |-  ( ( A e. B /\ B ~~ 1o ) -> { A } = B )
16 15 eqcomd 
 |-  ( ( A e. B /\ B ~~ 1o ) -> B = { A } )