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 V Rel A A V × V

Proof

Step Hyp Ref Expression
1 df-rel Rel A A V × V
2 snssg A V A V × V A V × V
3 1 2 bitr4id A V Rel A A V × V