Theorem elxp2 5572

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 463	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
2	1	2exbii 1843	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
3		elxp 5571	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
4		r2ex 3301	. 2 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
5	2, 3, 4	3bitr4i 305	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = ⟨𝑥, 𝑦⟩)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1531  ∃wex 1774   ∈ wcel 2108  ∃wrex 3137  ⟨cop 4565   × cxp 5546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-opab 5120  df-xp 5554

This theorem is referenced by:  opelxp  5584  xpiundi  5615  xpiundir  5616  ssrel2  5652  reuop  6137  el2xptp  7727  f1o2ndf1  7810  xpdom2  8604  tskxpss  10186  nqereu  10343  elreal  10545  efgmnvl  18832  frgpuptinv  18889  frgpup3lem  18895  ucnima  22882  ltgseg  26374  suppovss  30418  qtophaus  31093  esum2dlem  31344  bj-mpomptALT  34403  fourierdlem42  42424