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

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

Proof of Theorem ralrab
StepHypRef Expression
1 ralab.1 . . . . 5
21elrab 3257 . . . 4
32imbi1i 325 . . 3
4 impexp 446 . . 3
53, 4bitri 249 . 2
65ralbii2 2886 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  A.wral 2807  {crab 2811
This theorem is referenced by:  frminex  4864  wereu2  4881  weniso  6250  zmin  11207  prmreclem1  14434  lublecllem  15618  mhmeql  15995  ghmeql  16289  pgpfac1lem5  17130  lmhmeql  17701  islindf4  18873  1stcfb  19946  fbssfi  20338  filssufilg  20412  txflf  20507  ptcmplem3  20554  symgtgp  20600  tgpconcompeqg  20610  cnllycmp  21456  ovolgelb  21891  dyadmax  22007  lhop1  22415  radcnvlt1  22813  uvtxnb  24497  2spotdisj  25061  ismblfin  30055  igenval2  30463  mgmhmeql  32491  glbconN  35101
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-rab 2816  df-v 3111
  Copyright terms: Public domain W3C validator