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

Theorem 2rexbidv 2586
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2rexbidv  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)    A( x, y)    B( x, y)

Proof of Theorem 2rexbidv
StepHypRef Expression
1 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21rexbidv 2564 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2564 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wrex 2544
This theorem is referenced by:  f1oiso  5848  elrnmpt2g  5956  elrnmpt2  5957  ralrnmpt2  5958  ovelrn  5996  opiota  6290  omeu  6583  oeeui  6600  eroveu  6753  erov  6755  elfiun  7183  dffi3  7184  xpwdomg  7299  brdom7disj  8156  brdom6disj  8157  genpv  8623  genpelv  8624  axcnre  8786  supmullem1  9720  supmullem2  9721  supmul  9722  sqrlem6  11733  ello1  11989  ello1mpt  11995  elo1  12000  lo1o1  12006  o1lo1  12011  bezoutlem1  12717  bezoutlem3  12719  bezoutlem4  12720  bezout  12721  pythagtriplem2  12870  pythagtriplem19  12886  pythagtrip  12887  pcval  12897  pceu  12899  pczpre  12900  pcdiv  12905  4sqlem2  12996  4sqlem3  12997  4sqlem4  12999  4sq  13011  vdwlem1  13028  vdwlem12  13039  vdwlem13  13040  vdwnnlem1  13042  vdwnnlem2  13043  vdwnnlem3  13044  vdwnn  13045  ramub2  13061  rami  13062  pgpfac1lem3  15312  lspprel  15847  znunit  16517  hausnei  17056  isreg2  17105  txuni2  17260  txbas  17262  xkoopn  17284  txcls  17299  txcnpi  17302  txdis1cn  17329  txtube  17334  txcmplem1  17335  hausdiag  17339  tx1stc  17344  regr1lem2  17431  divstgplem  17803  met2ndci  18068  dyadmax  18953  i1fadd  19050  i1fmul  19051  elply  19577  2sqlem2  20603  2sqlem8  20611  2sqlem9  20612  2sqlem11  20614  cvmliftlem15  23829  cvmlift2lem10  23843  br8  24113  br6  24114  br4  24115  nofulllem5  24360  elaltxp  24509  axsegconlem1  24545  axpasch  24569  axlowdim  24589  axeuclidlem  24590  brsegle  24731  ellines  24775  intopcoaconlem3b  25538  intopcoaconlem3  25539  exopcopn  25572  elhaltdp2  26068  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  nn0prpwlem  26238  nn0prpw  26239  mzpcompact2lem  26829  mzpcompact2  26830  sbc4rexg  26866  pell1qrval  26931  elpell1qr  26932  pell14qrval  26933  elpell14qr  26934  pell1234qrval  26935  elpell1234qr  26936  jm2.27  27101  expdiophlem1  27114  isline  29928  psubspi  29936  paddfval  29986  elpadd  29988  paddvaln0N  29990
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator