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 >. }