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

Theorem ssneld 3997
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 (𝜑𝐴𝐵)
Assertion
Ref Expression
ssneld (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))

Proof of Theorem ssneld
StepHypRef Expression
1 ssneld.1 . . 3 (𝜑𝐴𝐵)
21sseld 3994 . 2 (𝜑 → (𝐶𝐴𝐶𝐵))
32con3d 152 1 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2106  wss 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814  df-ss 3980
This theorem is referenced by:  ssneldd  3998  kmlem2  10190  hashbclem  14488  prodss  15980  coprmproddvdslem  16696  mrissmrid  17686  mpfrcl  22127  onsuct0  36424  ftc1anc  37688  dvhdimlem  41427  dvh3dim2  41431  dvh3dim3N  41432  mapdh9a  41772  hdmapval0  41816  hdmap11lem2  41825  iundjiunlem  46415  elbigolo1  48407
  Copyright terms: Public domain W3C validator