Metamath Proof Explorer


Theorem relsnopg

Description: A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998) (Revised by BJ, 12-Feb-2022)

Ref Expression
Assertion relsnopg
|- ( ( A e. V /\ B e. W ) -> Rel { <. A , B >. } )

Proof

Step Hyp Ref Expression
1 opelvvg
 |-  ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )
2 opex
 |-  <. A , B >. e. _V
3 relsng
 |-  ( <. A , B >. e. _V -> ( Rel { <. A , B >. } <-> <. A , B >. e. ( _V X. _V ) ) )
4 2 3 mp1i
 |-  ( ( A e. V /\ B e. W ) -> ( Rel { <. A , B >. } <-> <. A , B >. e. ( _V X. _V ) ) )
5 1 4 mpbird
 |-  ( ( A e. V /\ B e. W ) -> Rel { <. A , B >. } )