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