Theorem elxp 5679

Description: Membership in a Cartesian product. (Contributed by NM, 4-Jul-1994.)

Assertion

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

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

Proof of Theorem elxp

Step	Hyp	Ref	Expression
1		df-xp 5662	. . 3 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
2	1	eleq2i 2856	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
3		elopab 5506	. 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
4	2, 3	bitri 278	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ⟨cop 4838  {copab 5171   × cxp 5654

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 5253  ax-pr 5396

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-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5172  df-xp 5662

This theorem is used by:  elxp2  5680  0nelxp  5690  0nelelxp  5691  rabxp  5704  elxp3  5722  elvvOLD  5732  elvvv  5733  dfres3  5987  xpdifid  6172  xpdifcnvepel  6173  dfco2a  6261  elsnxp  6315  tpres  7233  elxp4  7961  elxp5  7962  opabex3d  8004  opabex3rd  8005  opabex3  8006  xp1st  8060  xp2nd  8061  poxp  8170  soxp  8171  xpsnen  9111  xpcomco  9117  xpassen  9121  dfac5lem1  10232  dfac5lem4  10235  axdc4lem  10563  fsum2dlem  15968  fprod2dlem  16179  mgmn0plusgf  18859  mgmn0plusgplusf  18860  numclwwlk1lem2fo  30992  satefvfmla0  36363  elima4  36731  brcart  36885  brimg  36890  dibelval3  42407