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

Theorem ralab 3246
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 2798 . 2  |-  ( A. x  e.  { y  |  ph } ch  <->  A. x
( x  e.  {
y  |  ph }  ->  ch ) )
2 vex 3098 . . . . 5  |-  x  e. 
_V
3 ralab.1 . . . . 5  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
42, 3elab 3232 . . . 4  |-  ( x  e.  { y  | 
ph }  <->  ps )
54imbi1i 325 . . 3  |-  ( ( x  e.  { y  |  ph }  ->  ch )  <->  ( ps  ->  ch ) )
65albii 1627 . 2  |-  ( A. x ( x  e. 
{ y  |  ph }  ->  ch )  <->  A. x
( ps  ->  ch ) )
71, 6bitri 249 1  |-  ( A. x  e.  { y  |  ph } ch  <->  A. x
( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1381    e. wcel 1804   {cab 2428   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097
This theorem is referenced by:  ralrnmpt2  6402  funcnvuni  6738  kardex  8315  karden  8316  fimaxre3  10499  ptcnp  20100  ptrescn  20117  itg2leub  22118  nmoubi  25663  nmopub  26803  nmfnleub  26820  nmcexi  26921  mblfinlem3  30028  ismblfin  30030  itg2addnc  30044  hbtlem2  31048
  Copyright terms: Public domain W3C validator