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

Theorem rexralbidv 2759
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 2735 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2736 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 2715   E.wrex 2716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2720  df-rex 2721
This theorem is referenced by:  freq1  4690  rexfiuz  12835  cau3lem  12842  caubnd2  12845  climi  12988  rlimi  12991  o1lo1  13015  2clim  13050  lo1le  13129  caucvgrlem  13150  caurcvgr  13151  caucvgb  13157  vdwlem10  14051  vdwlem13  14054  neiptopnei  18736  lmcvg  18866  lmss  18902  elpt  19145  elptr  19146  txlm  19221  tsmsi  19704  ustuqtop4  19819  isucn  19853  isucn2  19854  ucnima  19856  metcnpi  20119  metcnpi2  20120  metucnOLD  20163  metucn  20164  xrge0tsms  20411  elcncf  20465  cncfi  20470  lmmcvg  20772  lhop1  21486  ulmval  21845  ulmi  21851  ulmcaulem  21859  ulmdvlem3  21867  pntibnd  22842  pntlem3  22858  pntleml  22860  axtgcont1  22929  isperp  23103  brbtwn  23145  isgrpo  23683  ubthlem3  24273  ubth  24274  hcau  24586  hcaucvg  24588  hlimi  24590  hlimconvi  24593  hlim2  24594  elcnop  25261  elcnfn  25286  cnopc  25317  cnfnc  25334  lnopcon  25439  lnfncon  25460  riesz1  25469  xrge0tsmsd  26253  signsply0  26952  pmatcollpw2lem  30905
  Copyright terms: Public domain W3C validator