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

Theorem elxp 5708
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 5691 . . 3 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
21eleq2i 2833 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
3 elopab 5532 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
42, 3bitri 275 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  cop 4632  {copab 5205   × cxp 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691
This theorem is referenced by:  elxp2  5709  0nelxp  5719  0nelelxp  5720  rabxp  5733  elxp3  5751  elvv  5760  elvvv  5761  0xp  5784  dfres3  6002  xpdifid  6188  dfco2a  6266  elsnxp  6311  tpres  7221  elxp4  7944  elxp5  7945  opabex3d  7990  opabex3rd  7991  opabex3  7992  xp1st  8046  xp2nd  8047  poxp  8153  soxp  8154  xpsnen  9095  xpcomco  9102  xpassen  9106  dfac5lem1  10163  dfac5lem4  10166  dfac5lem4OLD  10168  axdc4lem  10495  fsum2dlem  15806  fprod2dlem  16016  numclwwlk1lem2fo  30377  satefvfmla0  35423  elima4  35776  brcart  35933  brimg  35938  dibelval3  41149
  Copyright terms: Public domain W3C validator