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

Theorem ssneld 3505
 Description: If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
ssneld.1
Assertion
Ref Expression
ssneld

Proof of Theorem ssneld
StepHypRef Expression
1 ssneld.1 . . 3
21sseld 3502 . 2
32con3d 133 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  e.wcel 1818  C_wss 3475 This theorem is referenced by:  ssneldd  3506  kmlem2  8552  hashbclem  12501  prodss  13754  mrissmrid  15038  mpfrcl  18187  onsuct0  29906  ftc1anc  30098  dvhdimlem  37171  dvh3dim2  37175  dvh3dim3N  37176  mapdh9a  37517  hdmapval0  37563  hdmap11lem2  37572 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-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator