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

Theorem ralrab 3258
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 3254 . . . 4  |-  ( x  e.  { y  e.  A  |  ph }  <->  ( x  e.  A  /\  ps ) )
32imbi1i 323 . . 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 2883 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 367    e. wcel 1823   A.wral 2804   {crab 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rab 2813  df-v 3108
This theorem is referenced by:  frminex  4848  wereu2  4865  weniso  6225  zmin  11179  prmreclem1  14518  lublecllem  15817  mhmeql  16194  ghmeql  16488  pgpfac1lem5  17325  lmhmeql  17896  islindf4  19040  1stcfb  20112  fbssfi  20504  filssufilg  20578  txflf  20673  ptcmplem3  20720  symgtgp  20766  tgpconcompeqg  20776  cnllycmp  21622  ovolgelb  22057  dyadmax  22173  lhop1  22581  radcnvlt1  22979  uvtxnb  24699  2spotdisj  25263  ismblfin  30295  igenval2  30703  mgmhmeql  32863  glbconN  35498
  Copyright terms: Public domain W3C validator