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

Theorem rexralbidv 2710
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 2686 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2687 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 2666   E.wrex 2667
This theorem is referenced by:  freq1  4512  rexfiuz  12106  cau3lem  12113  caubnd2  12116  climi  12259  rlimi  12262  o1lo1  12286  2clim  12321  lo1le  12400  caucvgrlem  12421  caurcvgr  12422  caucvgb  12428  vdwlem10  13313  vdwlem13  13316  neiptopnei  17151  lmcvg  17280  lmss  17316  elpt  17557  elptr  17558  txlm  17633  tsmsi  18116  ustuqtop4  18227  isucn  18261  isucn2  18262  ucnima  18264  metcnpi  18527  metcnpi2  18528  metucnOLD  18571  metucn  18572  xrge0tsms  18818  elcncf  18872  cncfi  18877  lmmcvg  19167  lhop1  19851  ulmval  20249  ulmi  20255  ulmcaulem  20263  ulmdvlem3  20271  pntibnd  21240  pntlem3  21256  pntleml  21258  isgrpo  21737  ubthlem3  22327  ubth  22328  hcau  22639  hcaucvg  22641  hlimi  22643  hlimconvi  22646  hlim2  22647  elcnop  23313  elcnfn  23338  cnopc  23369  cnfnc  23386  lnopcon  23491  lnfncon  23512  riesz1  23521  xrge0tsmsd  24176  brbtwn  25742
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 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator