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

Theorem ssneldd 3364
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  |-  ( ph  ->  A  C_  B )
ssneldd.2  |-  ( ph  ->  -.  C  e.  B
)
Assertion
Ref Expression
ssneldd  |-  ( ph  ->  -.  C  e.  A
)

Proof of Theorem ssneldd
StepHypRef Expression
1 ssneldd.2 . 2  |-  ( ph  ->  -.  C  e.  B
)
2 ssneld.1 . . 3  |-  ( ph  ->  A  C_  B )
32ssneld 3363 . 2  |-  ( ph  ->  ( -.  C  e.  B  ->  -.  C  e.  A ) )
41, 3mpd 15 1  |-  ( ph  ->  -.  C  e.  A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1756    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347
This theorem is referenced by:  cantnfp1lem3  7893  cantnfp1lem3OLD  7919  fpwwe2lem13  8814  pwfseqlem3  8832  hashbclem  12210  sumrblem  13193  incexclem  13304  ramub1lem2  14093  mreexmrid  14586  mreexexlem2d  14588  acsfiindd  15352  lbspss  17168  lbsextlem4  17247  lindfrn  18255  fclscmpi  19607  lhop2  21492  lhop  21493  dvcnvrelem1  21494  axlowdimlem17  23209  erdszelem8  27091  prodrblem  27447  fprodntriv  27460  osumcllem10N  33614  pexmidlem7N  33625  mapdindp2  35371  mapdindp3  35372  hdmapval3lemN  35490  hdmap11lem1  35494
  Copyright terms: Public domain W3C validator