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

Metamath Proof Explorer

Theorem elxp3

Description: Membership in a Cartesian product. (Contributed by NM, 5-Mar-1995)

Ref Expression
Assertion elxp3 ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 elxp ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
2 eqcom ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ↔ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
3 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
4 2 3 anbi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
5 4 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
6 1 5 bitr4i ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )