Metamath Proof Explorer


Theorem en1eqsnbi

Description: A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr . (Contributed by FL, 13-Feb-2010) (Revised by AV, 25-Jan-2020)

Ref Expression
Assertion en1eqsnbi
|- ( A e. B -> ( B ~~ 1o <-> B = { A } ) )

Proof

Step Hyp Ref Expression
1 en1eqsn
 |-  ( ( A e. B /\ B ~~ 1o ) -> B = { A } )
2 1 ex
 |-  ( A e. B -> ( B ~~ 1o -> B = { A } ) )
3 ensn1g
 |-  ( A e. B -> { A } ~~ 1o )
4 breq1
 |-  ( B = { A } -> ( B ~~ 1o <-> { A } ~~ 1o ) )
5 3 4 syl5ibrcom
 |-  ( A e. B -> ( B = { A } -> B ~~ 1o ) )
6 2 5 impbid
 |-  ( A e. B -> ( B ~~ 1o <-> B = { A } ) )