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

Theorem 2rexbidv 2599
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 2577 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2577 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 2557
This theorem is referenced by:  f1oiso  5864  elrnmpt2g  5972  elrnmpt2  5973  ralrnmpt2  5974  ovelrn  6012  opiota  6306  omeu  6599  oeeui  6616  eroveu  6769  erov  6771  elfiun  7199  dffi3  7200  xpwdomg  7315  brdom7disj  8172  brdom6disj  8173  genpv  8639  genpelv  8640  axcnre  8802  supmullem1  9736  supmullem2  9737  supmul  9738  sqrlem6  11749  ello1  12005  ello1mpt  12011  elo1  12016  lo1o1  12022  o1lo1  12027  bezoutlem1  12733  bezoutlem3  12735  bezoutlem4  12736  bezout  12737  pythagtriplem2  12886  pythagtriplem19  12902  pythagtrip  12903  pcval  12913  pceu  12915  pczpre  12916  pcdiv  12921  4sqlem2  13012  4sqlem3  13013  4sqlem4  13015  4sq  13027  vdwlem1  13044  vdwlem12  13055  vdwlem13  13056  vdwnnlem1  13058  vdwnnlem2  13059  vdwnnlem3  13060  vdwnn  13061  ramub2  13077  rami  13078  pgpfac1lem3  15328  lspprel  15863  znunit  16533  hausnei  17072  isreg2  17121  txuni2  17276  txbas  17278  xkoopn  17300  txcls  17315  txcnpi  17318  txdis1cn  17345  txtube  17350  txcmplem1  17351  hausdiag  17355  tx1stc  17360  regr1lem2  17447  divstgplem  17819  met2ndci  18084  dyadmax  18969  i1fadd  19066  i1fmul  19067  elply  19593  2sqlem2  20619  2sqlem8  20627  2sqlem9  20628  2sqlem11  20630  cvmliftlem15  23844  cvmlift2lem10  23858  br8  24184  br6  24185  br4  24186  nofulllem5  24431  elaltxp  24581  axsegconlem1  24617  axpasch  24641  axlowdim  24661  axeuclidlem  24662  brsegle  24803  ellines  24847  supadd  24996  itg2addnc  25005  intopcoaconlem3b  25641  intopcoaconlem3  25642  exopcopn  25675  elhaltdp2  26171  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  nn0prpwlem  26341  nn0prpw  26342  mzpcompact2lem  26932  mzpcompact2  26933  sbc4rexg  26969  pell1qrval  27034  elpell1qr  27035  pell14qrval  27036  elpell14qr  27037  pell1234qrval  27038  elpell1234qr  27039  jm2.27  27204  expdiophlem1  27217  nb3grapr  28289  isline  30550  psubspi  30558  paddfval  30608  elpadd  30610  paddvaln0N  30612
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-rex 2562
  Copyright terms: Public domain W3C validator