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

Theorem 2rexbidv 2973
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2rexbidv.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 2rexbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21rexbidv 2966 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2966 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 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-rex 2813
This theorem is referenced by:  f1oiso  6226  elrnmpt2g  6389  elrnmpt2  6390  ralrnmpt2  6392  ovelrn  6426  opiota  6833  omeu  7224  oeeui  7241  eroveu  7396  erov  7398  elfiun  7879  dffi3  7880  xpwdomg  8000  brdom7disj  8898  brdom6disj  8899  genpv  9366  genpelv  9367  axcnre  9530  supmullem1  10498  supmullem2  10499  supmul  10500  sqrlem6  13031  ello1  13287  ello1mpt  13293  elo1  13298  lo1o1  13304  o1lo1  13309  bezoutlem1  14024  bezoutlem3  14026  bezoutlem4  14027  bezout  14028  pythagtriplem2  14189  pythagtriplem19  14205  pythagtrip  14206  pcval  14216  pceu  14218  pczpre  14219  pcdiv  14224  4sqlem2  14315  4sqlem3  14316  4sqlem4  14318  4sq  14330  vdwlem1  14347  vdwlem12  14358  vdwlem13  14359  vdwnnlem1  14361  vdwnnlem2  14362  vdwnnlem3  14363  vdwnn  14364  ramub2  14380  rami  14381  pgpfac1lem3  16911  lspprel  17516  znunit  18362  cayleyhamiltonALT  19152  hausnei  19588  isreg2  19637  txuni2  19794  txbas  19796  xkoopn  19818  txcls  19833  txcnpi  19837  txdis1cn  19864  txtube  19869  txcmplem1  19870  hausdiag  19874  tx1stc  19879  regr1lem2  19969  divstgplem  20347  met2ndci  20753  dyadmax  21735  i1fadd  21830  i1fmul  21831  elply  22320  2sqlem2  23360  2sqlem8  23368  2sqlem9  23369  2sqlem11  23371  axtgeucl  23591  legov  23692  axsegconlem1  23889  axpasch  23913  axlowdim  23933  axeuclidlem  23934  nb3grapr  24115  el2wlksoton  24540  el2spthsoton  24541  el2wlksotot  24544  br8d  26986  pstmval  27360  eulerpartlemgh  27807  eulerpartlemgs2  27809  cvmliftlem15  28233  cvmlift2lem10  28247  br8  28612  br6  28613  br4  28614  nofulllem5  28893  elaltxp  29052  brsegle  29185  ellines  29229  supadd  29469  ptrest  29476  ismblfin  29483  itg2addnclem3  29496  itg2addnc  29497  nn0prpwlem  29568  nn0prpw  29569  mzpcompact2lem  30139  mzpcompact2  30140  sbc4rexgOLD  30178  pell1qrval  30237  elpell1qr  30238  pell14qrval  30239  elpell14qr  30240  pell1234qrval  30241  elpell1234qr  30242  jm2.27  30407  expdiophlem1  30420  fourierdlem48  31274  vdn0frgrav2  31742  vdgn0frgrav2  31743  vdn1frgrav2  31744  vdgn1frgrav2  31745  usg2spot2nb  31784  isline  34410  psubspi  34418  paddfval  34468  elpadd  34470  paddvaln0N  34472
  Copyright terms: Public domain W3C validator