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 ) )