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

Theorem elxp2 4967
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 2805 . . . 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 2981 . . . 4  |-  ( E. y  e.  C  ( x  e.  B  /\  A  =  <. x ,  y >. )  <->  ( x  e.  B  /\  E. y  e.  C  A  =  <. x ,  y >.
) )
3 an13 797 . . . . 5  |-  ( ( y  e.  C  /\  ( x  e.  B  /\  A  =  <. x ,  y >. )
)  <->  ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
43exbii 1635 . . . 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 275 . . 3  |-  ( ( x  e.  B  /\  E. y  e.  C  A  =  <. x ,  y
>. )  <->  E. y ( A  =  <. x ,  y
>.  /\  ( x  e.  B  /\  y  e.  C ) ) )
65exbii 1635 . 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 2805 . 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 4966 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. x E. y ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
96, 7, 83bitr4ri 278 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 184    /\ wa 369    = wceq 1370   E.wex 1587    e. wcel 1758   E.wrex 2800   <.cop 3992    X. cxp 4947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pr 4640
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rex 2805  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-opab 4460  df-xp 4955
This theorem is referenced by:  opelxp  4978  xpiundi  5002  xpiundir  5003  ssrel2  5039  f1o2ndf1  6791  xpdom2  7517  tskxpss  9051  nqereu  9210  elreal  9410  xpnnenOLD  13611  efgmnvl  16333  frgpuptinv  16390  frgpup3lem  16396  ucnima  19989  el2xptp  30275
  Copyright terms: Public domain W3C validator