Theorem elxp2 5709

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

Assertion

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

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem elxp2

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070  ⟨cop 4632   × cxp 5683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691

This theorem is referenced by:  opelxp  5721  xpiundi  5756  xpiundir  5757  ssrel2  5795  reuop  6313  el2xptp  8060  f1o2ndf1  8147  frpoins3xpg  8165  poxp2  8168  xpord2pred  8170  sexp2  8171  xpdom2  9107  tskxpss  10812  nqereu  10969  elreal  11171  xpsmnd0  18791  efgmnvl  19732  frgpuptinv  19789  frgpup3lem  19795  xpsring1d  20330  pzriprnglem3  21494  pzriprnglem8  21499  pzriprnglem10  21501  ucnima  24290  ltgseg  28604  suppovss  32690  elrlocbasi  33270  qtophaus  33835  esum2dlem  34093  bj-mpomptALT  37120  fourierdlem42  46164  gpgvtxel  48005