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

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

Proof of Theorem ssneld
StepHypRef Expression
1 ssneld.1 . . 3  |-  ( ph  ->  A  C_  B )
21sseld 3349 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32con3d 128 1  |-  ( ph  ->  ( -.  C  e.  B  ->  -.  C  e.  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  ssneldd  3353  kmlem2  8033  hashbclem  11703  mrissmrid  13868  mpfrcl  19941  prodss  25275  onsuct0  26193  ftc1anc  26290  dvhdimlem  32304  dvh3dim2  32308  dvh3dim3N  32309  mapdh9a  32650  hdmapval0  32696  hdmap11lem2  32705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator