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

Theorem ssneldd 3977
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 3976 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2098  wss 3940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957
This theorem is referenced by:  0nelrel0  5726  cantnfp1lem3  9670  fpwwe2lem12  10632  pwfseqlem3  10650  hashbclem  14407  sumrblem  15653  incexclem  15778  prodrblem  15869  fprodntriv  15882  ramub1lem2  16956  mreexmrid  17583  mreexexlem2d  17585  acsfiindd  18505  lbspss  20915  lbsextlem4  20997  lindfrn  21676  fclscmpi  23843  lhop2  25858  lhop  25859  dvcnvrelem1  25860  axlowdimlem17  28640  cyc3co2  32726  erdszelem8  34644  bj-fununsn1  36590  bj-fvsnun2  36593  poimirlem16  36960  osumcllem10N  39292  pexmidlem7N  39303  mapdindp2  41048  mapdindp3  41049  hdmapval3lemN  41164  hdmap11lem1  41168  fourierdlem80  45353
  Copyright terms: Public domain W3C validator