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

Theorem ssneld 3444
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 3441 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32con3d 133 1  |-  ( ph  ->  ( -.  C  e.  B  ->  -.  C  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1842    C_ wss 3414
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 3421  df-ss 3428
This theorem is referenced by:  ssneldd  3445  kmlem2  8563  hashbclem  12550  prodss  13906  mrissmrid  15255  mpfrcl  18507  onsuct0  30673  ftc1anc  31471  dvhdimlem  34464  dvh3dim2  34468  dvh3dim3N  34469  mapdh9a  34810  hdmapval0  34856  hdmap11lem2  34865  elbigolo1  38688
  Copyright terms: Public domain W3C validator