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

Theorem elxp 5661
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 5644 . . 3 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
21eleq2i 2830 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
3 elopab 5489 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
42, 3bitri 275 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  cop 4597  {copab 5172   × cxp 5636
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-xp 5644
This theorem is referenced by:  elxp2  5662  0nelxp  5672  0nelelxp  5673  rabxp  5685  elxp3  5703  elvv  5711  elvvv  5712  0xp  5735  dfres3  5947  xpdifid  6125  dfco2a  6203  elsnxp  6248  tpres  7155  elxp4  7864  elxp5  7865  opabex3d  7903  opabex3rd  7904  opabex3  7905  xp1st  7958  xp2nd  7959  poxp  8065  soxp  8066  xpsnen  9006  xpcomco  9013  xpassen  9017  dfac5lem1  10066  dfac5lem4  10069  axdc4lem  10398  fsum2dlem  15662  fprod2dlem  15870  numclwwlk1lem2fo  29344  satefvfmla0  34052  elima4  34389  brcart  34546  brimg  34551  dibelval3  39639
  Copyright terms: Public domain W3C validator