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
Assertion
Ref Expression
ralab
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)   ()   (,)

Proof of Theorem ralab
StepHypRef Expression
1 df-ral 2798 . 2
2 vex 3098 . . . . 5
3 ralab.1 . . . . 5
42, 3elab 3232 . . . 4
54imbi1i 325 . . 3
65albii 1627 . 2
71, 6bitri 249 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184  wal 1381   wcel 1804  cab 2428  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