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

Step	Hyp	Ref	Expression
1		ralab.1	. . . . 5
2	1	elrab 3257	. . . 4
3	2	imbi1i 325	. . 3
4		impexp 446	. . 3
5	3, 4	bitri 249	. 2
6	5	ralbii2 2886	1

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