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

Theorem 2rexbidv 2740
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 2718 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2718 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 2698
This theorem is referenced by:  f1oiso  6063  elrnmpt2g  6174  elrnmpt2  6175  ralrnmpt2  6176  ovelrn  6214  opiota  6527  omeu  6820  oeeui  6837  eroveu  6991  erov  6993  elfiun  7427  dffi3  7428  xpwdomg  7545  brdom7disj  8401  brdom6disj  8402  genpv  8868  genpelv  8869  axcnre  9031  supmullem1  9966  supmullem2  9967  supmul  9968  sqrlem6  12045  ello1  12301  ello1mpt  12307  elo1  12312  lo1o1  12318  o1lo1  12323  bezoutlem1  13030  bezoutlem3  13032  bezoutlem4  13033  bezout  13034  pythagtriplem2  13183  pythagtriplem19  13199  pythagtrip  13200  pcval  13210  pceu  13212  pczpre  13213  pcdiv  13218  4sqlem2  13309  4sqlem3  13310  4sqlem4  13312  4sq  13324  vdwlem1  13341  vdwlem12  13352  vdwlem13  13353  vdwnnlem1  13355  vdwnnlem2  13356  vdwnnlem3  13357  vdwnn  13358  ramub2  13374  rami  13375  pgpfac1lem3  15627  lspprel  16158  znunit  16836  hausnei  17384  isreg2  17433  txuni2  17589  txbas  17591  xkoopn  17613  txcls  17628  txcnpi  17632  txdis1cn  17659  txtube  17664  txcmplem1  17665  hausdiag  17669  tx1stc  17674  regr1lem2  17764  divstgplem  18142  met2ndci  18544  dyadmax  19482  i1fadd  19579  i1fmul  19580  elply  20106  2sqlem2  21140  2sqlem8  21148  2sqlem9  21149  2sqlem11  21151  nb3grapr  21454  pstmval  24282  cvmliftlem15  24977  cvmlift2lem10  24991  br8  25371  br6  25372  br4  25373  nofulllem5  25653  elaltxp  25812  axsegconlem1  25848  axpasch  25872  axlowdim  25892  axeuclidlem  25893  brsegle  26034  ellines  26078  supadd  26229  ismblfin  26237  itg2addnclem3  26248  itg2addnc  26249  nn0prpwlem  26316  nn0prpw  26317  mzpcompact2lem  26799  mzpcompact2  26800  sbc4rexg  26836  pell1qrval  26900  elpell1qr  26901  pell14qrval  26902  elpell14qr  26903  pell1234qrval  26904  elpell1234qr  26905  jm2.27  27070  expdiophlem1  27083  el2wlksoton  28298  el2spthsoton  28299  el2wlksotot  28302  vdn0frgrav2  28351  vdgn0frgrav2  28352  vdn1frgrav2  28353  vdgn1frgrav2  28354  usg2spot2nb  28391  isline  30473  psubspi  30481  paddfval  30531  elpadd  30533  paddvaln0N  30535
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-rex 2703
  Copyright terms: Public domain W3C validator