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

Theorem 2rexbidv 2694
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 2672 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2672 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 177   E.wrex 2652
This theorem is referenced by:  f1oiso  6012  elrnmpt2g  6123  elrnmpt2  6124  ralrnmpt2  6125  ovelrn  6163  opiota  6473  omeu  6766  oeeui  6783  eroveu  6937  erov  6939  elfiun  7372  dffi3  7373  xpwdomg  7488  brdom7disj  8344  brdom6disj  8345  genpv  8811  genpelv  8812  axcnre  8974  supmullem1  9908  supmullem2  9909  supmul  9910  sqrlem6  11982  ello1  12238  ello1mpt  12244  elo1  12249  lo1o1  12255  o1lo1  12260  bezoutlem1  12967  bezoutlem3  12969  bezoutlem4  12970  bezout  12971  pythagtriplem2  13120  pythagtriplem19  13136  pythagtrip  13137  pcval  13147  pceu  13149  pczpre  13150  pcdiv  13155  4sqlem2  13246  4sqlem3  13247  4sqlem4  13249  4sq  13261  vdwlem1  13278  vdwlem12  13289  vdwlem13  13290  vdwnnlem1  13292  vdwnnlem2  13293  vdwnnlem3  13294  vdwnn  13295  ramub2  13311  rami  13312  pgpfac1lem3  15564  lspprel  16095  znunit  16769  hausnei  17316  isreg2  17365  txuni2  17520  txbas  17522  xkoopn  17544  txcls  17559  txcnpi  17563  txdis1cn  17590  txtube  17595  txcmplem1  17596  hausdiag  17600  tx1stc  17605  regr1lem2  17695  divstgplem  18073  met2ndci  18444  dyadmax  19359  i1fadd  19456  i1fmul  19457  elply  19983  2sqlem2  21017  2sqlem8  21025  2sqlem9  21026  2sqlem11  21028  nb3grapr  21330  cvmliftlem15  24766  cvmlift2lem10  24780  br8  25139  br6  25140  br4  25141  nofulllem5  25386  elaltxp  25536  axsegconlem1  25572  axpasch  25596  axlowdim  25616  axeuclidlem  25617  brsegle  25758  ellines  25802  supadd  25950  itg2addnc  25961  nn0prpwlem  26018  nn0prpw  26019  mzpcompact2lem  26501  mzpcompact2  26502  sbc4rexg  26538  pell1qrval  26602  elpell1qr  26603  pell14qrval  26604  elpell14qr  26605  pell1234qrval  26606  elpell1234qr  26607  jm2.27  26772  expdiophlem1  26785  vdn0frgrav2  27779  vdgn0frgrav2  27780  vdn1frgrav2  27781  vdgn1frgrav2  27782  isline  29855  psubspi  29863  paddfval  29913  elpadd  29915  paddvaln0N  29917
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-rex 2657
  Copyright terms: Public domain W3C validator