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

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 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 elxp2 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 opth2 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 = 𝑥 ∧ 𝐵 = 𝑦 ) )
5 eleq1 ⊢ ( 𝐴 = 𝑥 → ( 𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶 ) )
6 eleq1 ⊢ ( 𝐵 = 𝑦 → ( 𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷 ) )
7 5 6 bi2anan9 ⊢ ( ( 𝐴 = 𝑥 ∧ 𝐵 = 𝑦 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
8 4 7 sylbi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
9 8 biimprcd ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) )
10 9 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )
11 eqid ⊢ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩
12 opeq1 ⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
13 12 eqeq2d ⊢ ( 𝑥 = 𝐴 → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ ) )
14 opeq2 ⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
15 14 eqeq2d ⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
16 13 15 rspc2ev ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
17 11 16 mp3an3 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
18 10 17 impbii ⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )
19 1 18 bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )