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

Theorem ssneldd 3918
 Description: If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
ssneld.1 (𝜑𝐴𝐵)
ssneldd.2 (𝜑 → ¬ 𝐶𝐵)
Assertion
Ref Expression
ssneldd (𝜑 → ¬ 𝐶𝐴)

Proof of Theorem ssneldd
StepHypRef Expression
1 ssneldd.2 . 2 (𝜑 → ¬ 𝐶𝐵)
2 ssneld.1 . . 3 (𝜑𝐴𝐵)
32ssneld 3917 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ⊆ wss 3881 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898 This theorem is referenced by:  0nelrel0  5576  cantnfp1lem3  9129  fpwwe2lem12  10055  pwfseqlem3  10073  hashbclem  13808  sumrblem  15062  incexclem  15185  prodrblem  15277  fprodntriv  15290  ramub1lem2  16355  mreexmrid  16908  mreexexlem2d  16910  acsfiindd  17781  lbspss  19850  lbsextlem4  19929  lindfrn  20514  fclscmpi  22641  lhop2  24625  lhop  24626  dvcnvrelem1  24627  axlowdimlem17  26759  cyc3co2  30839  erdszelem8  32570  bj-fununsn1  34684  bj-fvsnun2  34687  osumcllem10N  37277  pexmidlem7N  37288  mapdindp2  39033  mapdindp3  39034  hdmapval3lemN  39149  hdmap11lem1  39153  fourierdlem80  42843
 Copyright terms: Public domain W3C validator