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

Theorem 2rexbidv 2748
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 2726 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2726 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-rex 2711
This theorem is referenced by:  f1oiso  6029  elrnmpt2g  6191  elrnmpt2  6192  ralrnmpt2  6194  ovelrn  6228  opiota  6622  omeu  7012  oeeui  7029  eroveu  7183  erov  7185  elfiun  7668  dffi3  7669  xpwdomg  7788  brdom7disj  8686  brdom6disj  8687  genpv  9155  genpelv  9156  axcnre  9318  supmullem1  10283  supmullem2  10284  supmul  10285  sqrlem6  12720  ello1  12976  ello1mpt  12982  elo1  12987  lo1o1  12993  o1lo1  12998  bezoutlem1  13704  bezoutlem3  13706  bezoutlem4  13707  bezout  13708  pythagtriplem2  13866  pythagtriplem19  13882  pythagtrip  13883  pcval  13893  pceu  13895  pczpre  13896  pcdiv  13901  4sqlem2  13992  4sqlem3  13993  4sqlem4  13995  4sq  14007  vdwlem1  14024  vdwlem12  14035  vdwlem13  14036  vdwnnlem1  14038  vdwnnlem2  14039  vdwnnlem3  14040  vdwnn  14041  ramub2  14057  rami  14058  pgpfac1lem3  16551  lspprel  17096  znunit  17837  hausnei  18773  isreg2  18822  txuni2  18979  txbas  18981  xkoopn  19003  txcls  19018  txcnpi  19022  txdis1cn  19049  txtube  19054  txcmplem1  19055  hausdiag  19059  tx1stc  19064  regr1lem2  19154  divstgplem  19532  met2ndci  19938  dyadmax  20919  i1fadd  21014  i1fmul  21015  elply  21547  2sqlem2  22587  2sqlem8  22595  2sqlem9  22596  2sqlem11  22598  axtgeucl  22817  legov  22891  axsegconlem1  22985  axpasch  23009  axlowdim  23029  axeuclidlem  23030  nb3grapr  23183  br8d  25765  pstmval  26175  eulerpartlemgh  26608  eulerpartlemgs2  26610  cvmliftlem15  27034  cvmlift2lem10  27048  br8  27412  br6  27413  br4  27414  nofulllem5  27693  elaltxp  27852  brsegle  27985  ellines  28029  supadd  28259  ptrest  28266  ismblfin  28273  itg2addnclem3  28286  itg2addnc  28287  nn0prpwlem  28358  nn0prpw  28359  mzpcompact2lem  28930  mzpcompact2  28931  sbc4rexgOLD  28970  pell1qrval  29029  elpell1qr  29030  pell14qrval  29031  elpell14qr  29032  pell1234qrval  29033  elpell1234qr  29034  jm2.27  29199  expdiophlem1  29212  el2wlksoton  30240  el2spthsoton  30241  el2wlksotot  30244  vdn0frgrav2  30459  vdgn0frgrav2  30460  vdn1frgrav2  30461  vdgn1frgrav2  30462  usg2spot2nb  30501  isline  32953  psubspi  32961  paddfval  33011  elpadd  33013  paddvaln0N  33015
  Copyright terms: Public domain W3C validator