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

Theorem 2rexbidv 2961
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 2954 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2954 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 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-rex 2799
This theorem is referenced by:  f1oiso  6232  elrnmpt2g  6399  elrnmpt2  6400  ralrnmpt2  6402  ovelrn  6436  opiota  6844  omeu  7236  oeeui  7253  eroveu  7408  erov  7410  elfiun  7892  dffi3  7893  xpwdomg  8014  brdom7disj  8912  brdom6disj  8913  genpv  9380  genpelv  9381  axcnre  9544  supmullem1  10515  supmullem2  10516  supmul  10517  sqrlem6  13060  ello1  13317  ello1mpt  13323  elo1  13328  lo1o1  13334  o1lo1  13339  bezoutlem1  14053  bezoutlem3  14055  bezoutlem4  14056  bezout  14057  pythagtriplem2  14218  pythagtriplem19  14234  pythagtrip  14235  pcval  14245  pceu  14247  pczpre  14248  pcdiv  14253  4sqlem2  14344  4sqlem3  14345  4sqlem4  14347  4sq  14359  vdwlem1  14376  vdwlem12  14387  vdwlem13  14388  vdwnnlem1  14390  vdwnnlem2  14391  vdwnnlem3  14392  vdwnn  14393  ramub2  14409  rami  14410  pgpfac1lem3  17002  lspprel  17614  znunit  18475  cayleyhamiltonALT  19265  hausnei  19702  isreg2  19751  txuni2  19939  txbas  19941  xkoopn  19963  txcls  19978  txcnpi  19982  txdis1cn  20009  txtube  20014  txcmplem1  20015  hausdiag  20019  tx1stc  20024  regr1lem2  20114  qustgplem  20492  met2ndci  20898  dyadmax  21880  i1fadd  21975  i1fmul  21976  elply  22465  2sqlem2  23511  2sqlem8  23519  2sqlem9  23520  2sqlem11  23522  istrkgld  23729  axtgeucl  23742  legov  23844  axsegconlem1  24092  axpasch  24116  axlowdim  24136  axeuclidlem  24137  nb3grapr  24325  el2wlksoton  24750  el2spthsoton  24751  el2wlksotot  24754  2wot2wont  24758  vdn0frgrav2  24895  vdgn0frgrav2  24896  vdn1frgrav2  24897  vdgn1frgrav2  24898  usg2spot2nb  24937  br8d  27335  pstmval  27747  eulerpartlemgh  28190  eulerpartlemgs2  28192  cvmliftlem15  28616  cvmlift2lem10  28630  br8  29160  br6  29161  br4  29162  nofulllem5  29441  elaltxp  29600  brsegle  29733  ellines  29777  supadd  30017  ptrest  30023  ismblfin  30030  itg2addnclem3  30043  itg2addnc  30044  nn0prpwlem  30115  nn0prpw  30116  mzpcompact2lem  30659  mzpcompact2  30660  sbc4rexgOLD  30698  pell1qrval  30757  elpell1qr  30758  pell14qrval  30759  elpell14qr  30760  pell1234qrval  30761  elpell1234qr  30762  jm2.27  30925  expdiophlem1  30938  limclner  31565  fourierdlem42  31820  fourierdlem48  31826  isline  35203  psubspi  35211  paddfval  35261  elpadd  35263  paddvaln0N  35265
  Copyright terms: Public domain W3C validator