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

Theorem elxp 4856
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 4845 . . 3  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
21eleq2i 2541 . 2  |-  ( A  e.  ( B  X.  C )  <->  A  e.  {
<. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
3 elopab 4709 . 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 257 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 189    /\ wa 376    = wceq 1452   E.wex 1671    e. wcel 1904   <.cop 3965   {copab 4453    X. cxp 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-opab 4455  df-xp 4845
This theorem is referenced by:  elxp2  4857  0nelxp  4867  0nelelxp  4868  rabxp  4876  elxp3  4890  elvv  4898  elvvv  4899  0xp  4920  xpdifid  5271  dfco2a  5342  elsnxp  5385  tpres  6133  elxp4  6756  elxp5  6757  opabex3d  6790  opabex3  6791  xp1st  6842  xp2nd  6843  poxp  6927  soxp  6928  xpsnen  7674  xpcomco  7680  xpassen  7684  dfac5lem1  8572  dfac5lem4  8575  axdc4lem  8903  fsum2dlem  13908  fprod2dlem  14111  numclwlk1lem2fo  25902  dfres3  30470  elima4  30492  brcart  30770  brimg  30775  dibelval3  34786
  Copyright terms: Public domain W3C validator