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

Theorem rexralbidv 2947
Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2rexbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rexralbidv  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. 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 rexralbidv
StepHypRef Expression
1 2rexbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ralbidv 2864 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2939 1  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wral 2775   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781
This theorem is referenced by:  freq1  4820  rexfiuz  13399  cau3lem  13406  caubnd2  13409  climi  13562  rlimi  13565  o1lo1  13589  2clim  13624  lo1le  13703  caucvgrlem  13724  caucvgrlemOLD  13725  caurcvgr  13726  caurcvgrOLD  13727  caucvgb  13734  vdwlem10  14928  vdwlem13  14931  pmatcollpw2lem  19788  neiptopnei  20135  lmcvg  20265  lmss  20301  elpt  20574  elptr  20575  txlm  20650  tsmsi  21135  ustuqtop4  21246  isucn  21280  isucn2  21281  ucnima  21283  metcnpi  21546  metcnpi2  21547  metucn  21573  xrge0tsms  21839  elcncf  21908  cncfi  21913  lmmcvg  22218  lhop1  22953  ulmval  23322  ulmi  23328  ulmcaulem  23336  ulmdvlem3  23344  pntibnd  24418  pntlem3  24434  pntleml  24436  axtgcont1  24503  perpln1  24742  perpln2  24743  isperp  24744  brbtwn  24916  isgrpo  25910  ubthlem3  26500  ubth  26501  hcau  26823  hcaucvg  26825  hlimi  26827  hlimconvi  26830  hlim2  26831  elcnop  27496  elcnfn  27521  cnopc  27552  cnfnc  27569  lnopcon  27674  lnfncon  27695  riesz1  27704  xrge0tsmsd  28544  signsply0  29436  limcleqr  37545  addlimc  37549  0ellimcdiv  37550  cncfshift  37571  cncfperiod  37576  ioodvbdlimc1lem1  37623  ioodvbdlimc1lem2  37624  ioodvbdlimc1lem1OLD  37625  ioodvbdlimc1lem2OLD  37626  ioodvbdlimc2lem  37628  ioodvbdlimc2lemOLD  37629  fourierdlem68  37858  fourierdlem87  37877  fourierdlem103  37893  fourierdlem104  37894  etransclem48OLD  37967  etransclem48  37968
  Copyright terms: Public domain W3C validator