Description: A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | relsn.1 | |- A e. _V |
|
Assertion | relsn | |- ( Rel { A } <-> A e. ( _V X. _V ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relsn.1 | |- A e. _V |
|
2 | relsng | |- ( A e. _V -> ( Rel { A } <-> A e. ( _V X. _V ) ) ) |
|
3 | 1 2 | ax-mp | |- ( Rel { A } <-> A e. ( _V X. _V ) ) |