Metamath Proof Explorer

Theorem opelvvg

Description: Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015)

Ref Expression
Assertion opelvvg 
|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 elex 
 |-  ( B e. W -> B e. _V )
3 opelxpi 
 |-  ( ( A e. _V /\ B e. _V ) -> <. A , B >. e. ( _V X. _V ) )
4 1 2 3 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )