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 𝐴𝐶
opelxpii.2 𝐵𝐷
Assertion opelxpii 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 )

Proof

Step Hyp Ref Expression
1 opelxpii.1 𝐴𝐶
2 opelxpii.2 𝐵𝐷
3 opelxpi ( ( 𝐴𝐶𝐵𝐷 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) )
4 1 2 3 mp2an 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 )