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

Theorem ssrab 3577
 Description: Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
Assertion
Ref Expression
ssrab
Distinct variable groups:   ,   ,

Proof of Theorem ssrab
StepHypRef Expression
1 df-rab 2816 . . 3
21sseq2i 3528 . 2
3 ssab 3569 . 2
4 dfss3 3493 . . . 4
54anbi1i 695 . . 3
6 r19.26 2984 . . 3
7 df-ral 2812 . . 3
85, 6, 73bitr2ri 274 . 2
92, 3, 83bitri 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:  ssrabdv  3578  omssnlim  6714  ordtypelem2  7965  ordtypelem10  7973  card2inf  8002  r0weon  8411  ramtlecl  14518  sscntz  16364  ppttop  19508  epttop  19510  cmpcov2  19890  tgcmp  19901  xkoinjcn  20188  fbssfi  20338  filssufilg  20412  uffixfr  20424  tmdgsum2  20595  symgtgp  20600  ghmcnp  20613  blcls  21009  clsocv  21690  lhop1lem  22414  ressatans  23265  axcontlem3  24269  axcontlem4  24270  imambfm  28233  conpcon  28680  cvmlift2lem11  28758  cvmlift2lem12  28759  hbtlem6  31078  bj-rabtr  34497 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