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

Theorem ralrab 3088
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 3084 . . . 4  |-  ( x  e.  { y  e.  A  |  ph }  <->  ( x  e.  A  /\  ps ) )
32imbi1i 316 . . 3  |-  ( ( x  e.  { y  e.  A  |  ph }  ->  ch )  <->  ( (
x  e.  A  /\  ps )  ->  ch )
)
4 impexp 434 . . 3  |-  ( ( ( x  e.  A  /\  ps )  ->  ch ) 
<->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
53, 4bitri 241 . 2  |-  ( ( x  e.  { y  e.  A  |  ph }  ->  ch )  <->  ( x  e.  A  ->  ( ps 
->  ch ) ) )
65ralbii2 2725 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 177    /\ wa 359    e. wcel 1725   A.wral 2697   {crab 2701
This theorem is referenced by:  frminex  4554  wereu2  4571  weniso  6067  zmin  10562  prmreclem1  13276  lubid  14431  mhmeql  14756  ghmeql  15020  pgpfac1lem5  15629  lmhmeql  16123  1stcfb  17500  fbssfi  17861  filssufilg  17935  txflf  18030  ptcmplem3  18077  symgtgp  18123  tgpconcompeqg  18133  cnllycmp  18973  ovolgelb  19368  dyadmax  19482  lhop1  19890  radcnvlt1  20326  ismblfin  26237  igenval2  26667  islindf4  27276  2spotdisj  28387  glbconN  30111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rab 2706  df-v 2950
  Copyright terms: Public domain W3C validator