Metamath Proof Explorer

Theorem relsng

Description: A singleton is a relation iff it is a singleton on an ordered pair. (Contributed by NM, 24-Sep-2013) (Revised by BJ, 12-Feb-2022)

Ref Expression
Assertion relsng 
|- ( A e. V -> ( Rel { A } <-> A e. ( _V X. _V ) ) )

Proof

Step Hyp Ref Expression
1 df-rel 
 |-  ( Rel { A } <-> { A } C_ ( _V X. _V ) )
2 snssg 
 |-  ( A e. V -> ( A e. ( _V X. _V ) <-> { A } C_ ( _V X. _V ) ) )
3 1 2 bitr4id 
 |-  ( A e. V -> ( Rel { A } <-> A e. ( _V X. _V ) ) )