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

Theorem rexralbidv 2981
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 2903 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2973 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 184   A.wral 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  freq1  4849  rexfiuz  13142  cau3lem  13149  caubnd2  13152  climi  13295  rlimi  13298  o1lo1  13322  2clim  13357  lo1le  13436  caucvgrlem  13457  caurcvgr  13458  caucvgb  13464  vdwlem10  14366  vdwlem13  14369  pmatcollpw2lem  19061  neiptopnei  19415  lmcvg  19545  lmss  19581  elpt  19824  elptr  19825  txlm  19900  tsmsi  20383  ustuqtop4  20498  isucn  20532  isucn2  20533  ucnima  20535  metcnpi  20798  metcnpi2  20799  metucnOLD  20842  metucn  20843  xrge0tsms  21090  elcncf  21144  cncfi  21149  lmmcvg  21451  lhop1  22166  ulmval  22525  ulmi  22531  ulmcaulem  22539  ulmdvlem3  22547  pntibnd  23522  pntlem3  23538  pntleml  23540  axtgcont1  23609  perpln1  23811  perpln2  23812  isperp  23813  brbtwn  23894  isgrpo  24890  ubthlem3  25480  ubth  25481  hcau  25793  hcaucvg  25795  hlimi  25797  hlimconvi  25800  hlim2  25801  elcnop  26468  elcnfn  26493  cnopc  26524  cnfnc  26541  lnopcon  26646  lnfncon  26667  riesz1  26676  xrge0tsmsd  27454  signsply0  28164  0ellimcdiv  31207  ioodvbdlimc1lem2  31278  ioodvbdlimc2lem  31280  fourierdlem68  31491  fourierdlem103  31526  fourierdlem104  31527
  Copyright terms: Public domain W3C validator