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

Theorem ssneldd 3566
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 3565 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1975  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
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 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-in 3542  df-ss 3549
This theorem is referenced by:  cantnfp1lem3  8433  fpwwe2lem13  9316  pwfseqlem3  9334  hashbclem  13041  sumrblem  14231  incexclem  14349  prodrblem  14440  fprodntriv  14453  ramub1lem2  15511  mreexmrid  16068  mreexexlem2d  16070  acsfiindd  16942  lbspss  18845  lbsextlem4  18924  lindfrn  19917  fclscmpi  21581  lhop2  23495  lhop  23496  dvcnvrelem1  23497  axlowdimlem17  25552  erdszelem8  30236  osumcllem10N  34068  pexmidlem7N  34079  mapdindp2  35827  mapdindp3  35828  hdmapval3lemN  35946  hdmap11lem1  35950  fourierdlem80  38879
  Copyright terms: Public domain W3C validator