MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elxp2 Structured version   Visualization version   GIF version

Theorem elxp2 5613
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
StepHypRef Expression
1 ancom 461 . . 3 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ((𝑥𝐵𝑦𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
212exbii 1851 . 2 (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑥𝑦((𝑥𝐵𝑦𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
3 elxp 5612 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
4 r2ex 3232 . 2 (∃𝑥𝐵𝑦𝐶 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦((𝑥𝐵𝑦𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
52, 3, 43bitr4i 303 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝐵𝑦𝐶 𝐴 = ⟨𝑥, 𝑦⟩)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2106  wrex 3065  cop 4567   × cxp 5587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-xp 5595
This theorem is referenced by:  opelxp  5625  xpiundi  5657  xpiundir  5658  ssrel2  5696  reuop  6196  el2xptp  7877  f1o2ndf1  7963  xpdom2  8854  tskxpss  10528  nqereu  10685  elreal  10887  efgmnvl  19320  frgpuptinv  19377  frgpup3lem  19383  ucnima  23433  ltgseg  26957  suppovss  31017  qtophaus  31786  esum2dlem  32060  elxpxp  33683  frpoins3xpg  33787  poxp2  33790  xpord2pred  33792  sexp2  33793  bj-mpomptALT  35290  fourierdlem42  43690
  Copyright terms: Public domain W3C validator