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

Theorem ralrab 3110
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 3106 . . . 4  |-  ( x  e.  { y  e.  A  |  ph }  <->  ( x  e.  A  /\  ps ) )
32imbi1i 325 . . 3  |-  ( ( x  e.  { y  e.  A  |  ph }  ->  ch )  <->  ( (
x  e.  A  /\  ps )  ->  ch )
)
4 impexp 444 . . 3  |-  ( ( ( x  e.  A  /\  ps )  ->  ch ) 
<->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
53, 4bitri 249 . 2  |-  ( ( x  e.  { y  e.  A  |  ph }  ->  ch )  <->  ( x  e.  A  ->  ( ps 
->  ch ) ) )
65ralbii2 2733 1  |-  ( A. x  e.  { y  e.  A  |  ph } ch 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1755   A.wral 2705   {crab 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rab 2714  df-v 2964
This theorem is referenced by:  frminex  4687  wereu2  4704  weniso  6032  zmin  10937  prmreclem1  13960  lublecllem  15141  mhmeql  15474  ghmeql  15749  pgpfac1lem5  16554  lmhmeql  17058  islindf4  18109  1stcfb  18891  fbssfi  19252  filssufilg  19326  txflf  19421  ptcmplem3  19468  symgtgp  19514  tgpconcompeqg  19524  cnllycmp  20370  ovolgelb  20805  dyadmax  20920  lhop1  21328  radcnvlt1  21768  ismblfin  28276  igenval2  28710  uvtxnb  30124  2spotdisj  30500  glbconN  32594
  Copyright terms: Public domain W3C validator