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

Theorem rexralbidv 2600
Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.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 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ralbidv 2576 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2577 1  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2556   E.wrex 2557
This theorem is referenced by:  freq1  4379  rexfiuz  11847  cau3lem  11854  caubnd2  11857  climi  12000  rlimi  12003  o1lo1  12027  2clim  12062  lo1le  12141  caucvgrlem  12161  caurcvgr  12162  caucvgb  12168  vdwlem10  13053  vdwlem13  13056  lmcvg  17008  lmss  17042  elpt  17283  elptr  17284  txlm  17358  tsmsi  17832  metcnpi  18106  metcnpi2  18107  xrge0tsms  18355  elcncf  18409  cncfi  18414  lmmcvg  18703  lhop1  19377  ulmval  19775  ulmi  19781  ulmcaulem  19787  ulmdvlem3  19795  pntibnd  20758  pntlem3  20774  pntleml  20776  isgrpo  20879  ubthlem3  21467  ubth  21468  hcau  21779  hcaucvg  21781  hlimi  21783  hlimconvi  21786  hlim2  21787  elcnop  22453  elcnfn  22478  cnopc  22509  cnfnc  22526  lnopcon  22631  lnfncon  22652  riesz1  22661  xrge0tsmsd  23397  brbtwn  24599
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator