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

Theorem elxp2 4851
Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004.)
Assertion
Ref Expression
elxp2  |-  ( A  e.  ( B  X.  C )  <->  E. x  e.  B  E. y  e.  C  A  =  <. x ,  y >.
)
Distinct variable groups:    x, y, A    x, B, y    x, C, y

Proof of Theorem elxp2
StepHypRef Expression
1 df-rex 2742 . . . 4  |-  ( E. y  e.  C  ( x  e.  B  /\  A  =  <. x ,  y >. )  <->  E. y
( y  e.  C  /\  ( x  e.  B  /\  A  =  <. x ,  y >. )
) )
2 r19.42v 2944 . . . 4  |-  ( E. y  e.  C  ( x  e.  B  /\  A  =  <. x ,  y >. )  <->  ( x  e.  B  /\  E. y  e.  C  A  =  <. x ,  y >.
) )
3 an13 807 . . . . 5  |-  ( ( y  e.  C  /\  ( x  e.  B  /\  A  =  <. x ,  y >. )
)  <->  ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
43exbii 1717 . . . 4  |-  ( E. y ( y  e.  C  /\  ( x  e.  B  /\  A  =  <. x ,  y
>. ) )  <->  E. y
( A  =  <. x ,  y >.  /\  (
x  e.  B  /\  y  e.  C )
) )
51, 2, 43bitr3i 279 . . 3  |-  ( ( x  e.  B  /\  E. y  e.  C  A  =  <. x ,  y
>. )  <->  E. y ( A  =  <. x ,  y
>.  /\  ( x  e.  B  /\  y  e.  C ) ) )
65exbii 1717 . 2  |-  ( E. x ( x  e.  B  /\  E. y  e.  C  A  =  <. x ,  y >.
)  <->  E. x E. y
( A  =  <. x ,  y >.  /\  (
x  e.  B  /\  y  e.  C )
) )
7 df-rex 2742 . 2  |-  ( E. x  e.  B  E. y  e.  C  A  =  <. x ,  y
>. 
<->  E. x ( x  e.  B  /\  E. y  e.  C  A  =  <. x ,  y
>. ) )
8 elxp 4850 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. x E. y ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
96, 7, 83bitr4ri 282 1  |-  ( A  e.  ( B  X.  C )  <->  E. x  e.  B  E. y  e.  C  A  =  <. x ,  y >.
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371    = wceq 1443   E.wex 1662    e. wcel 1886   E.wrex 2737   <.cop 3973    X. cxp 4831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-rex 2742  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-opab 4461  df-xp 4839
This theorem is referenced by:  opelxp  4863  xpiundi  4888  xpiundir  4889  ssrel2  4924  el2xptp  6833  f1o2ndf1  6901  xpdom2  7664  tskxpss  9194  nqereu  9351  elreal  9552  efgmnvl  17357  frgpuptinv  17414  frgpup3lem  17420  ucnima  21289  ltgseg  24634  qtophaus  28656  esum2dlem  28906  bj-mpt2mptALT  31624  fourierdlem42  38006  fourierdlem42OLD  38007
  Copyright terms: Public domain W3C validator