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