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

Theorem ralrab 2940
Description: Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypothesis
Ref Expression
ralab.1  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ralrab  |-  ( A. x  e.  { y  e.  A  |  ph } ch 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
Distinct variable groups:    x, y    y, A    ps, y
Allowed substitution hints:    ph( x, y)    ps( x)    ch( x, y)    A( x)

Proof of Theorem ralrab
StepHypRef Expression
1 ralab.1 . . . . 5  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
21elrab 2936 . . . 4  |-  ( x  e.  { y  e.  A  |  ph }  <->  ( x  e.  A  /\  ps ) )
32imbi1i 315 . . 3  |-  ( ( x  e.  { y  e.  A  |  ph }  ->  ch )  <->  ( (
x  e.  A  /\  ps )  ->  ch )
)
4 impexp 433 . . 3  |-  ( ( ( x  e.  A  /\  ps )  ->  ch ) 
<->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
53, 4bitri 240 . 2  |-  ( ( x  e.  { y  e.  A  |  ph }  ->  ch )  <->  ( x  e.  A  ->  ( ps 
->  ch ) ) )
65ralbii2 2584 1  |-  ( A. x  e.  { y  e.  A  |  ph } ch 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1696   A.wral 2556   {crab 2560
This theorem is referenced by:  frminex  4389  wereu2  4406  weniso  5868  zmin  10328  prmreclem1  12979  lubid  14132  mhmeql  14457  ghmeql  14721  pgpfac1lem5  15330  lmhmeql  15828  1stcfb  17187  fbssfi  17548  filssufilg  17622  txflf  17717  ptcmplem3  17764  symgtgp  17800  tgpconcompeqg  17810  cnllycmp  18470  ovolgelb  18855  dyadmax  18969  lhop1  19377  radcnvlt1  19810  ralrabOLD  26458  igenval2  26794  islindf4  27411  glbconN  30188
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565  df-v 2803
  Copyright terms: Public domain W3C validator