Theorem elxp2 5706

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 459	. . 3 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
2	1	2exbii 1844	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
3		elxp 5705	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
4		r2ex 3186	. 2 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
5	2, 3, 4	3bitr4i 302	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = ⟨𝑥, 𝑦⟩)

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1534  ∃wex 1774   ∈ wcel 2099  ∃wrex 3060  ⟨cop 4639   × cxp 5680

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 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-opab 5216  df-xp 5688

This theorem is referenced by:  opelxp  5718  xpiundi  5752  xpiundir  5753  ssrel2  5791  reuop  6304  el2xptp  8049  f1o2ndf1  8136  frpoins3xpg  8154  poxp2  8157  xpord2pred  8159  sexp2  8160  xpdom2  9105  tskxpss  10815  nqereu  10972  elreal  11174  xpsmnd0  18768  efgmnvl  19712  frgpuptinv  19769  frgpup3lem  19775  xpsring1d  20312  pzriprnglem3  21473  pzriprnglem8  21478  pzriprnglem10  21480  ucnima  24277  ltgseg  28523  suppovss  32597  elrlocbasi  33121  qtophaus  33651  esum2dlem  33925  bj-mpomptALT  36826  fourierdlem42  45770

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »