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

Theorem ssneldd 3351
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 3350 . 2  |-  ( ph  ->  ( -.  C  e.  B  ->  -.  C  e.  A ) )
41, 3mpd 15 1  |-  ( ph  ->  -.  C  e.  A
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1725    C_ wss 3320
This theorem is referenced by:  cantnfp1lem3  7636  fpwwe2lem13  8517  pwfseqlem3  8535  hashbclem  11701  sumrblem  12505  incexclem  12616  ramub1lem2  13395  mreexmrid  13868  mreexexlem2d  13870  acsfiindd  14603  lbspss  16154  lbsextlem4  16233  fclscmpi  18061  lhop2  19899  lhop  19900  dvcnvrelem1  19901  erdszelem8  24884  prodrblem  25255  fprodntriv  25268  axlowdimlem17  25897  lindfrn  27268  osumcllem10N  30762  pexmidlem7N  30773  mapdindp2  32519  mapdindp3  32520  hdmapval3lemN  32638  hdmap11lem1  32642
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator