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

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