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

Theorem ssneldd 3854
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 3853 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2051  wss 3822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-in 3829  df-ss 3836
This theorem is referenced by:  0nelrel0  5458  cantnfp1lem3  8935  fpwwe2lem13  9860  pwfseqlem3  9878  hashbclem  13621  sumrblem  14926  incexclem  15049  prodrblem  15141  fprodntriv  15154  ramub1lem2  16217  mreexmrid  16784  mreexexlem2d  16786  acsfiindd  17657  lbspss  19588  lbsextlem4  19667  lindfrn  20682  fclscmpi  22356  lhop2  24330  lhop  24331  dvcnvrelem1  24332  axlowdimlem17  26462  cyc3co2  30491  erdszelem8  32067  bj-fununsn1  34041  bj-fvsnun2  34044  osumcllem10N  36583  pexmidlem7N  36594  mapdindp2  38339  mapdindp3  38340  hdmapval3lemN  38455  hdmap11lem1  38459  fourierdlem80  41936
  Copyright terms: Public domain W3C validator