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

Theorem elxp 4959
Description: Membership in a Cartesian product. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
elxp  |-  ( A  e.  ( B  X.  C )  <->  E. x E. y ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
Distinct variable groups:    x, y, A    x, B, y    x, C, y

Proof of Theorem elxp
StepHypRef Expression
1 df-xp 4948 . . 3  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
21eleq2i 2480 . 2  |-  ( A  e.  ( B  X.  C )  <->  A  e.  {
<. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
3 elopab 4697 . 2  |-  ( A  e.  { <. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  (
x  e.  B  /\  y  e.  C )
) )
42, 3bitri 249 1  |-  ( A  e.  ( B  X.  C )  <->  E. x E. y ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    = wceq 1405   E.wex 1633    e. wcel 1842   <.cop 3977   {copab 4451    X. cxp 4940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-opab 4453  df-xp 4948
This theorem is referenced by:  elxp2  4960  0nelxp  4970  0nelelxp  4971  rabxp  4979  elxp3  4993  elvv  5001  elvvv  5002  0xp  5023  xpdifid  5374  dfco2a  5444  tpres  6060  elxp4  6682  elxp5  6683  opabex3d  6716  opabex3  6717  xp1st  6768  xp2nd  6769  poxp  6850  soxp  6851  xpsnen  7559  xpcomco  7565  xpassen  7569  dfac5lem1  8456  dfac5lem4  8459  axdc4lem  8787  fsum2dlem  13643  fprod2dlem  13843  numclwlk1lem2fo  25393  elsnxp  27786  dfres3  29858  elima4  29880  brcart  30243  brimg  30248  dibelval3  34148
  Copyright terms: Public domain W3C validator