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

Theorem elxp 5011
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 5000 . . 3  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
21eleq2i 2540 . 2  |-  ( A  e.  ( B  X.  C )  <->  A  e.  {
<. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
3 elopab 4750 . 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 369    = wceq 1374   E.wex 1591    e. wcel 1762   <.cop 4028   {copab 4499    X. cxp 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-opab 4501  df-xp 5000
This theorem is referenced by:  elxp2  5012  0nelxp  5021  0nelelxp  5022  rabxp  5030  elxp3  5044  elvv  5052  elvvv  5053  0xp  5073  xpdifid  5428  dfco2a  5500  elxp4  6720  elxp5  6721  opabex3d  6754  opabex3  6755  xp1st  6806  xp2nd  6807  poxp  6887  soxp  6888  xpsnen  7593  xpcomco  7599  xpassen  7603  dfac5lem1  8495  dfac5lem4  8498  axdc4lem  8826  fsum2dlem  13536  numclwlk1lem2fo  24760  fprod2dlem  28675  dfres3  28753  elima4  28774  brcart  29147  brimg  29152  dibelval3  35821
  Copyright terms: Public domain W3C validator