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

Theorem ssneld 3569
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 3566 . 2 (𝜑 → (𝐶𝐴𝐶𝐵))
32con3d 146 1 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1976  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  ssneldd  3570  kmlem2  8833  hashbclem  13047  prodss  14464  coprmproddvdslem  15162  mrissmrid  16072  mpfrcl  19287  onsuct0  31403  ftc1anc  32446  dvhdimlem  35534  dvh3dim2  35538  dvh3dim3N  35539  mapdh9a  35880  hdmapval0  35926  hdmap11lem2  35935  iundjiunlem  39135  elbigolo1  42130
  Copyright terms: Public domain W3C validator