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

Theorem ralab 3260
 Description: Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypothesis
Ref Expression
ralab.1
Assertion
Ref Expression
ralab
Distinct variable groups:   ,   ,

Proof of Theorem ralab
StepHypRef Expression
1 df-ral 2812 . 2
2 vex 3112 . . . . 5
3 ralab.1 . . . . 5
42, 3elab 3246 . . . 4
54imbi1i 325 . . 3
65albii 1640 . 2
71, 6bitri 249 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  {cab 2442  A.wral 2807 This theorem is referenced by:  ralrnmpt2  6417  funcnvuni  6753  kardex  8333  karden  8334  fimaxre3  10517  ptcnp  20123  ptrescn  20140  itg2leub  22141  nmoubi  25687  nmopub  26827  nmfnleub  26844  nmcexi  26945  mblfinlem3  30053  ismblfin  30055  itg2addnc  30069  hbtlem2  31073 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111
 Copyright terms: Public domain W3C validator