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

Theorem rabssdv 3579
Description: Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 2-Feb-2015.)
Hypothesis
Ref Expression
rabssdv.1
Assertion
Ref Expression
rabssdv
Distinct variable groups:   ,   ,

Proof of Theorem rabssdv
StepHypRef Expression
1 rabssdv.1 . . . 4
213exp 1195 . . 3
32ralrimiv 2869 . 2
4 rabss 3576 . 2
53, 4sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973  e.wcel 1818  A.wral 2807  {crab 2811  C_wss 3475
This theorem is referenced by:  suppss2OLD  6530  suppss2  6953  oemapvali  8124  cantnflem1  8129  cantnflem1OLD  8152  harval2  8399  zsupss  11200  ramub1lem1  14544  symggen  16495  efgsfo  16757  ablfacrp  17117  ablfac1eu  17124  pgpfac1lem5  17130  ablfaclem3  17138  nrmr0reg  20250  ptcmplem3  20554  abelthlem2  22827  lgamgulmlem1  28571  neibastop2lem  30178  topmeet  30182  cntotbnd  30292  mapdrvallem2  37372
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-3an 975  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