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

Theorem rabss 3576
Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
Assertion
Ref Expression
rabss
Distinct variable group:   ,

Proof of Theorem rabss
StepHypRef Expression
1 df-rab 2816 . . 3
21sseq1i 3527 . 2
3 abss 3568 . 2
4 impexp 446 . . . 4
54albii 1640 . . 3
6 df-ral 2812 . . 3
75, 6bitr4i 252 . 2
82, 3, 73bitri 271 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  e.wcel 1818  {cab 2442  A.wral 2807  {crab 2811  C_wss 3475
This theorem is referenced by:  rabssdv  3579  reusv6OLD  4663  fnsuppresOLD  6131  fnsuppres  6946  wemapso2OLD  7998  wemapso2lem  7999  tskwe2  9172  grothac  9229  uzwo3  11206  fsuppmapnn0fiub0  12099  phibndlem  14300  dfphi2  14304  ramval  14526  mgmidsssn0  15896  istopon  19426  ordtrest2lem  19704  filssufilg  20412  cfinufil  20429  blsscls2  21007  nmhmcn  21603  ovolshftlem2  21921  atansssdm  23264  sgmss  23380  sspval  25636  ubthlem2  25787  ordtrest2NEWlem  27904  truae  28215  dvtanlem  30064  nnubfi  30243  prnc  30464  itgperiod  31780  fourierdlem81  31970  usgresvm1  32443  usgresvm1ALT  32447
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-or 370  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-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator