Theorem eqsn

Description: Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	eqsn	|- ( A =/= (/) -> ( A = { B } <-> A. x e. A x = B ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	|- ( A =/= (/) <-> -. A = (/) )
2		biorf	|- ( -. A = (/) -> ( A = { B } <-> ( A = (/) \/ A = { B } ) ) )
3	1 2	sylbi	|- ( A =/= (/) -> ( A = { B } <-> ( A = (/) \/ A = { B } ) ) )
4		dfss3	|- ( A C_ { B } <-> A. x e. A x e. { B } )
5		sssn	|- ( A C_ { B } <-> ( A = (/) \/ A = { B } ) )
6		velsn	|- ( x e. { B } <-> x = B )
7	6	ralbii	|- ( A. x e. A x e. { B } <-> A. x e. A x = B )
8	4 5 7	3bitr3i	|- ( ( A = (/) \/ A = { B } ) <-> A. x e. A x = B )
9	3 8	bitrdi	|- ( A =/= (/) -> ( A = { B } <-> A. x e. A x = B ) )