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

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

Proof of Theorem ralab
StepHypRef Expression
1 df-ral 2561 . 2  |-  ( A. x  e.  { y  |  ph } ch  <->  A. x
( x  e.  {
y  |  ph }  ->  ch ) )
2 vex 2804 . . . . 5  |-  x  e. 
_V
3 ralab.1 . . . . 5  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
42, 3elab 2927 . . . 4  |-  ( x  e.  { y  | 
ph }  <->  ps )
54imbi1i 315 . . 3  |-  ( ( x  e.  { y  |  ph }  ->  ch )  <->  ( ps  ->  ch ) )
65albii 1556 . 2  |-  ( A. x ( x  e. 
{ y  |  ph }  ->  ch )  <->  A. x
( ps  ->  ch ) )
71, 6bitri 240 1  |-  ( A. x  e.  { y  |  ph } ch  <->  A. x
( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    e. wcel 1696   {cab 2282   A.wral 2556
This theorem is referenced by:  funcnvuni  5333  ralrnmpt2  5974  kardex  7580  karden  7581  fimaxre3  9719  ptcnp  17332  ptrescn  17349  itg2leub  19105  nmoubi  21366  nmopub  22504  nmfnleub  22521  nmcexi  22622  itg2addnc  25005  ralabOLD  26457  hbtlem2  27431
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-v 2803
  Copyright terms: Public domain W3C validator