Metamath Proof Explorer

Theorem relsnop

Description: A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses relsn.1 
|- A e. _V
relsnop.2 
|- B e. _V
Assertion relsnop 
|- Rel { <. A , B >. }

Proof

Step Hyp Ref Expression
1 relsn.1 
 |-  A e. _V
2 relsnop.2 
 |-  B e. _V
3 relsnopg 
 |-  ( ( A e. _V /\ B e. _V ) -> Rel { <. A , B >. } )
4 1 2 3 mp2an 
 |-  Rel { <. A , B >. }