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

Theorem ssneldd 3444
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 3443 . 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 1842    C_ wss 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3420  df-ss 3427
This theorem is referenced by:  cantnfp1lem3  8130  cantnfp1lem3OLD  8156  fpwwe2lem13  9049  pwfseqlem3  9067  hashbclem  12548  sumrblem  13680  incexclem  13797  prodrblem  13886  fprodntriv  13899  ramub1lem2  14752  mreexmrid  15255  mreexexlem2d  15257  acsfiindd  16129  lbspss  18046  lbsextlem4  18125  lindfrn  19146  fclscmpi  20820  lhop2  22706  lhop  22707  dvcnvrelem1  22708  axlowdimlem17  24665  erdszelem8  29482  osumcllem10N  32962  pexmidlem7N  32973  mapdindp2  34721  mapdindp3  34722  hdmapval3lemN  34840  hdmap11lem1  34844  fourierdlem80  37318
  Copyright terms: Public domain W3C validator