This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi 
 |-  ( 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 } )