Metamath Proof Explorer


Theorem relsn

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

Proof

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