# Metamath Proof Explorer

## Theorem opelxp

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opelxp $⊢ A B ∈ C × D ↔ A ∈ C ∧ B ∈ D$

### Proof

Step Hyp Ref Expression
1 elxp2 $⊢ A B ∈ C × D ↔ ∃ x ∈ C ∃ y ∈ D A B = x y$
2 vex $⊢ x ∈ V$
3 vex $⊢ y ∈ V$
4 2 3 opth2 $⊢ A B = x y ↔ A = x ∧ B = y$
5 eleq1 $⊢ A = x → A ∈ C ↔ x ∈ C$
6 eleq1 $⊢ B = y → B ∈ D ↔ y ∈ D$
7 5 6 bi2anan9 $⊢ A = x ∧ B = y → A ∈ C ∧ B ∈ D ↔ x ∈ C ∧ y ∈ D$
8 4 7 sylbi $⊢ A B = x y → A ∈ C ∧ B ∈ D ↔ x ∈ C ∧ y ∈ D$
9 8 biimprcd $⊢ x ∈ C ∧ y ∈ D → A B = x y → A ∈ C ∧ B ∈ D$
10 9 rexlimivv $⊢ ∃ x ∈ C ∃ y ∈ D A B = x y → A ∈ C ∧ B ∈ D$
11 eqid $⊢ A B = A B$
12 opeq1 $⊢ x = A → x y = A y$
13 12 eqeq2d $⊢ x = A → A B = x y ↔ A B = A y$
14 opeq2 $⊢ y = B → A y = A B$
15 14 eqeq2d $⊢ y = B → A B = A y ↔ A B = A B$
16 13 15 rspc2ev $⊢ A ∈ C ∧ B ∈ D ∧ A B = A B → ∃ x ∈ C ∃ y ∈ D A B = x y$
17 11 16 mp3an3 $⊢ A ∈ C ∧ B ∈ D → ∃ x ∈ C ∃ y ∈ D A B = x y$
18 10 17 impbii $⊢ ∃ x ∈ C ∃ y ∈ D A B = x y ↔ A ∈ C ∧ B ∈ D$
19 1 18 bitri $⊢ A B ∈ C × D ↔ A ∈ C ∧ B ∈ D$