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

Theorem rexralbidv 2694
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 2670 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2671 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 177   A.wral 2650   E.wrex 2651
This theorem is referenced by:  freq1  4494  rexfiuz  12079  cau3lem  12086  caubnd2  12089  climi  12232  rlimi  12235  o1lo1  12259  2clim  12294  lo1le  12373  caucvgrlem  12394  caurcvgr  12395  caucvgb  12401  vdwlem10  13286  vdwlem13  13289  neiptopnei  17120  lmcvg  17249  lmss  17285  elpt  17526  elptr  17527  txlm  17602  tsmsi  18085  ustuqtop4  18196  isucn  18230  isucn2  18231  ucnima  18233  metcnpi  18465  metcnpi2  18466  metucn  18491  xrge0tsms  18737  elcncf  18791  cncfi  18796  lmmcvg  19086  lhop1  19766  ulmval  20164  ulmi  20170  ulmcaulem  20178  ulmdvlem3  20186  pntibnd  21155  pntlem3  21171  pntleml  21173  isgrpo  21633  ubthlem3  22223  ubth  22224  hcau  22535  hcaucvg  22537  hlimi  22539  hlimconvi  22542  hlim2  22543  elcnop  23209  elcnfn  23234  cnopc  23265  cnfnc  23282  lnopcon  23387  lnfncon  23408  riesz1  23417  xrge0tsmsd  24053  brbtwn  25553
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2655  df-rex 2656
  Copyright terms: Public domain W3C validator