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

Theorem rexralbidv 2757
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 2733 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2734 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 2713   E.wrex 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-ral 2718  df-rex 2719
This theorem is referenced by:  freq1  4686  rexfiuz  12831  cau3lem  12838  caubnd2  12841  climi  12984  rlimi  12987  o1lo1  13011  2clim  13046  lo1le  13125  caucvgrlem  13146  caurcvgr  13147  caucvgb  13153  vdwlem10  14047  vdwlem13  14050  neiptopnei  18695  lmcvg  18825  lmss  18861  elpt  19104  elptr  19105  txlm  19180  tsmsi  19663  ustuqtop4  19778  isucn  19812  isucn2  19813  ucnima  19815  metcnpi  20078  metcnpi2  20079  metucnOLD  20122  metucn  20123  xrge0tsms  20370  elcncf  20424  cncfi  20429  lmmcvg  20731  lhop1  21445  ulmval  21804  ulmi  21810  ulmcaulem  21818  ulmdvlem3  21826  pntibnd  22801  pntlem3  22817  pntleml  22819  axtgcont1  22888  brbtwn  23080  isgrpo  23618  ubthlem3  24208  ubth  24209  hcau  24521  hcaucvg  24523  hlimi  24525  hlimconvi  24528  hlim2  24529  elcnop  25196  elcnfn  25221  cnopc  25252  cnfnc  25269  lnopcon  25374  lnfncon  25395  riesz1  25404  xrge0tsmsd  26188  signsply0  26882
  Copyright terms: Public domain W3C validator