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

Theorem ralab 3095
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 2710 . 2  |-  ( A. x  e.  { y  |  ph } ch  <->  A. x
( x  e.  {
y  |  ph }  ->  ch ) )
2 vex 2959 . . . . 5  |-  x  e. 
_V
3 ralab.1 . . . . 5  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
42, 3elab 3082 . . . 4  |-  ( x  e.  { y  | 
ph }  <->  ps )
54imbi1i 316 . . 3  |-  ( ( x  e.  { y  |  ph }  ->  ch )  <->  ( ps  ->  ch ) )
65albii 1575 . 2  |-  ( A. x ( x  e. 
{ y  |  ph }  ->  ch )  <->  A. x
( ps  ->  ch ) )
71, 6bitri 241 1  |-  ( A. x  e.  { y  |  ph } ch  <->  A. x
( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549    e. wcel 1725   {cab 2422   A.wral 2705
This theorem is referenced by:  funcnvuni  5518  ralrnmpt2  6184  kardex  7818  karden  7819  fimaxre3  9957  ptcnp  17654  ptrescn  17671  itg2leub  19626  nmoubi  22273  nmopub  23411  nmfnleub  23428  nmcexi  23529  mblfinlem3  26245  ismblfin  26247  itg2addnc  26259  hbtlem2  27305
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958
  Copyright terms: Public domain W3C validator