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

Theorem ssneld 3570
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 3567 . 2 (𝜑 → (𝐶𝐴𝐶𝐵))
32con3d 147 1 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1977  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  ssneldd  3571  kmlem2  8856  hashbclem  13093  prodss  14516  coprmproddvdslem  15214  mrissmrid  16124  mpfrcl  19339  onsuct0  31610  ftc1anc  32663  dvhdimlem  35751  dvh3dim2  35755  dvh3dim3N  35756  mapdh9a  36097  hdmapval0  36143  hdmap11lem2  36152  iundjiunlem  39352  elbigolo1  42149
  Copyright terms: Public domain W3C validator