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 e. B /\ B ~~ 1o ) -> B = { A } )

Proof

Step Hyp Ref Expression
1 en1
 |-  ( B ~~ 1o <-> E. x B = { x } )
2 eleq2
 |-  ( B = { x } -> ( A e. B <-> A e. { x } ) )
3 elsni
 |-  ( A e. { x } -> A = x )
4 3 sneqd
 |-  ( A e. { x } -> { A } = { x } )
5 2 4 syl6bi
 |-  ( B = { x } -> ( A e. B -> { A } = { x } ) )
6 5 imp
 |-  ( ( B = { x } /\ A e. B ) -> { A } = { x } )
7 eqtr3
 |-  ( ( B = { x } /\ { A } = { x } ) -> B = { A } )
8 6 7 syldan
 |-  ( ( B = { x } /\ A e. B ) -> B = { A } )
9 8 ex
 |-  ( B = { x } -> ( A e. B -> B = { A } ) )
10 9 exlimiv
 |-  ( E. x B = { x } -> ( A e. B -> B = { A } ) )
11 1 10 sylbi
 |-  ( B ~~ 1o -> ( A e. B -> B = { A } ) )
12 11 impcom
 |-  ( ( A e. B /\ B ~~ 1o ) -> B = { A } )