Metamath Proof Explorer
Description: Ordered pair membership in a Cartesian product (implication), induction
form. (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 |
⊢ 〈 𝐴 , 𝐵 〉 ∈ ( 𝐶 × 𝐷 ) |