Metamath Proof Explorer


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