Metamath Proof Explorer


Theorem elxp2

Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004) (Proof shortened by JJ, 13-Aug-2021)

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

Proof

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