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

Theorem rexralbidv 2587
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 2563 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2564 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 2543   E.wrex 2544
This theorem is referenced by:  freq1  4363  rexfiuz  11831  cau3lem  11838  caubnd2  11841  climi  11984  rlimi  11987  o1lo1  12011  2clim  12046  lo1le  12125  caucvgrlem  12145  caurcvgr  12146  caucvgb  12152  vdwlem10  13037  vdwlem13  13040  lmcvg  16992  lmss  17026  elpt  17267  elptr  17268  txlm  17342  tsmsi  17816  metcnpi  18090  metcnpi2  18091  xrge0tsms  18339  elcncf  18393  cncfi  18398  lmmcvg  18687  lhop1  19361  ulmval  19759  ulmi  19765  ulmcaulem  19771  ulmdvlem3  19779  pntibnd  20742  pntlem3  20758  pntleml  20760  isgrpo  20863  ubthlem3  21451  ubth  21452  hcau  21763  hcaucvg  21765  hlimi  21767  hlimconvi  21770  hlim2  21771  elcnop  22437  elcnfn  22462  cnopc  22493  cnfnc  22510  lnopcon  22615  lnfncon  22636  riesz1  22645  xrge0tsmsd  23382  brbtwn  24527
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator