This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelxpii

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

Ref Expression
Hypotheses opelxpii.1 ⊢ A ∈ C
opelxpii.2 ⊢ B ∈ D
Assertion opelxpii ⊢ A B ∈ C × D

Proof

Step Hyp Ref Expression
1 opelxpii.1 ⊢ A ∈ C
2 opelxpii.2 ⊢ B ∈ D
3 opelxpi ⊢ A ∈ C ∧ B ∈ D → A B ∈ C × D
4 1 2 3 mp2an ⊢ A B ∈ C × D