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

Theorem ssneldd 3506
Description: If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
ssneld.1
ssneldd.2
Assertion
Ref Expression
ssneldd

Proof of Theorem ssneldd
StepHypRef Expression
1 ssneldd.2 . 2
2 ssneld.1 . . 3
32ssneld 3505 . 2
41, 3mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  e.wcel 1818  C_wss 3475
This theorem is referenced by:  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  fpwwe2lem13  9041  pwfseqlem3  9059  hashbclem  12501  sumrblem  13533  incexclem  13648  prodrblem  13736  fprodntriv  13749  ramub1lem2  14545  mreexmrid  15040  mreexexlem2d  15042  acsfiindd  15807  lbspss  17728  lbsextlem4  17807  lindfrn  18856  fclscmpi  20530  lhop2  22416  lhop  22417  dvcnvrelem1  22418  axlowdimlem17  24261  erdszelem8  28642  fourierdlem80  31969  osumcllem10N  35689  pexmidlem7N  35700  mapdindp2  37448  mapdindp3  37449  hdmapval3lemN  37567  hdmap11lem1  37571
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