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