Theorem elxp2 5682

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 466	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
2	1	2exbii 1882	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
3		elxp 5681	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
4		r2ex 3203	. 2 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
5	2, 3, 4	3bitr4i 306	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = ⟨𝑥, 𝑦⟩)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090  ⟨cop 4840   × cxp 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-sn 4589  df-pr 4591  df-op 4841  df-opab 5174  df-xp 5664

This theorem is used by:  opelxp  5694  xpiundi  5729  xpiundir  5730  elvv  5733  ssrel2  5770  el2xptp  5830  reuop  6322  f1o2ndf1  8170  frpoins3xpg  8194  poxp2  8197  xpord2pred  8199  sexp2  8200  xpdom2  9129  tskxpss  10896  nqereu  11053  elreal  11255  xpsmnd0  19022  efgmnvl  19979  frgpuptinv  20036  frgpup3lem  20042  xpsring1d  20614  pzriprnglem3  21844  pzriprnglem8  21849  pzriprnglem10  21851  ucnima  24654  ltgseg  29116  suppovss  33371  elrlocbasi  33927  qtophaus  34579  esum2dlem  34835  bj-elinxp  38177  bj-mpomptALT  38311  fourierdlem42  47432  gpgvtxel  49418