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

Theorem elxp 5542
 Description: Membership in a Cartesian product. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
elxp (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem elxp
StepHypRef Expression
1 df-xp 5525 . . 3 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
21eleq2i 2881 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
3 elopab 5379 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
42, 3bitri 278 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ⟨cop 4531  {copab 5092   × cxp 5517 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525 This theorem is referenced by:  elxp2  5543  0nelxp  5553  0nelelxp  5554  rabxp  5564  elxp3  5582  elvv  5590  elvvv  5591  0xp  5613  dfres3  5823  xpdifid  5992  dfco2a  6066  elsnxp  6110  tpres  6940  elxp4  7611  elxp5  7612  opabex3d  7650  opabex3rd  7651  opabex3  7652  xp1st  7705  xp2nd  7706  poxp  7807  soxp  7808  xpsnen  8586  xpcomco  8592  xpassen  8596  dfac5lem1  9536  dfac5lem4  9539  axdc4lem  9868  fsum2dlem  15119  fprod2dlem  15328  numclwwlk1lem2fo  28150  satefvfmla0  32790  elima4  33144  brcart  33518  brimg  33523  dibelval3  38459
 Copyright terms: Public domain W3C validator