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

Theorem ralab 2926
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 2548 . 2  |-  ( A. x  e.  { y  |  ph } ch  <->  A. x
( x  e.  {
y  |  ph }  ->  ch ) )
2 vex 2791 . . . . 5  |-  x  e. 
_V
3 ralab.1 . . . . 5  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
42, 3elab 2914 . . . 4  |-  ( x  e.  { y  | 
ph }  <->  ps )
54imbi1i 315 . . 3  |-  ( ( x  e.  { y  |  ph }  ->  ch )  <->  ( ps  ->  ch ) )
65albii 1553 . 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 1527    e. wcel 1684   {cab 2269   A.wral 2543
This theorem is referenced by:  funcnvuni  5317  ralrnmpt2  5958  kardex  7564  karden  7565  fimaxre3  9703  ptcnp  17316  ptrescn  17333  itg2leub  19089  nmoubi  21350  nmopub  22488  nmfnleub  22505  nmcexi  22606  ralabOLD  26354  hbtlem2  27328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790
  Copyright terms: Public domain W3C validator