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