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 | ⊢ 〈 𝐴 , 𝐵 〉 ∈ ( 𝐶 × 𝐷 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxpii.1 | ⊢ 𝐴 ∈ 𝐶 | |
2 | opelxpii.2 | ⊢ 𝐵 ∈ 𝐷 | |
3 | opelxpi | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 〈 𝐴 , 𝐵 〉 ∈ ( 𝐶 × 𝐷 ) ) | |
4 | 1 2 3 | mp2an | ⊢ 〈 𝐴 , 𝐵 〉 ∈ ( 𝐶 × 𝐷 ) |