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

Theorem elxp 5285
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 5269 . . 3 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
21eleq2i 2845 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
3 elopab 5130 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
42, 3bitri 265 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 383   = wceq 1634  wex 1855  wcel 2148  cop 4332  {copab 4859   × cxp 5261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pr 5048
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-opab 4860  df-xp 5269
This theorem is referenced by:  elxp2  5286  0nelxp  5296  0nelelxp  5297  rabxp  5306  elxp3  5321  elvv  5329  elvvv  5330  0xp  5351  dfres3  5551  xpdifid  5714  dfco2a  5790  elsnxp  5832  tpres  6629  elxp4  7278  elxp5  7279  opabex3d  7313  opabex3  7314  xp1st  7368  xp2nd  7369  poxp  7461  soxp  7462  xpsnen  8221  xpcomco  8227  xpassen  8231  dfac5lem1  9167  dfac5lem4  9170  axdc4lem  9500  fsum2dlem  14731  fprod2dlem  14939  numclwwlk1lem2fo  27565  elima4  32032  brcart  32393  brimg  32398  dibelval3  36972
  Copyright terms: Public domain W3C validator