Metamath Proof Explorer

Theorem opelxpi

Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995)

Ref Expression
Assertion opelxpi 
|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )

Proof

Step Hyp Ref Expression
1 opelxp 
 |-  ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
2 1 biimpri 
 |-  ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )