Metamath Proof Explorer


Theorem opelxpii

Description: Ordered pair membership in a Cartesian product (implication). (Contributed by Steven Nguyen, 17-Jul-2022)

Ref Expression
Hypotheses opelxpii.1
|- A e. C
opelxpii.2
|- B e. D
Assertion opelxpii
|- <. A , B >. e. ( C X. D )

Proof

Step Hyp Ref Expression
1 opelxpii.1
 |-  A e. C
2 opelxpii.2
 |-  B e. D
3 opelxpi
 |-  ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )
4 1 2 3 mp2an
 |-  <. A , B >. e. ( C X. D )