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

Theorem ralrab 3265
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 3261 . . . 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 446 . . 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 2893 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 1767   A.wral 2814   {crab 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rab 2823  df-v 3115
This theorem is referenced by:  frminex  4859  wereu2  4876  weniso  6236  zmin  11174  prmreclem1  14289  lublecllem  15471  mhmeql  15805  ghmeql  16084  pgpfac1lem5  16920  lmhmeql  17484  islindf4  18640  1stcfb  19712  fbssfi  20073  filssufilg  20147  txflf  20242  ptcmplem3  20289  symgtgp  20335  tgpconcompeqg  20345  cnllycmp  21191  ovolgelb  21626  dyadmax  21742  lhop1  22150  radcnvlt1  22547  uvtxnb  24173  2spotdisj  24738  ismblfin  29632  igenval2  30066  glbconN  34173
  Copyright terms: Public domain W3C validator