Description: A singleton is a relation iff it has a nonempty domain. (Contributed by NM, 25-Sep-2013) Make hypothesis an antecedent. (Revised by BJ, 12-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | relsn2 | |- ( A e. V -> ( Rel { A } <-> dom { A } =/= (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relsng | |- ( A e. V -> ( Rel { A } <-> A e. ( _V X. _V ) ) ) |
|
| 2 | dmsnn0 | |- ( A e. ( _V X. _V ) <-> dom { A } =/= (/) ) |
|
| 3 | 1 2 | bitrdi | |- ( A e. V -> ( Rel { A } <-> dom { A } =/= (/) ) ) |