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

Theorem ssneldd 3986
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 3985 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2108  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968
This theorem is referenced by:  0nelrel0  5745  cantnfp1lem3  9720  fpwwe2lem12  10682  pwfseqlem3  10700  hashbclem  14491  sumrblem  15747  incexclem  15872  prodrblem  15965  fprodntriv  15978  ramub1lem2  17065  mreexmrid  17686  mreexexlem2d  17688  acsfiindd  18598  lbspss  21081  lbsextlem4  21163  lindfrn  21841  fclscmpi  24037  lhop2  26054  lhop  26055  dvcnvrelem1  26056  axlowdimlem17  28973  cyc3co2  33160  ssdifidlprm  33486  erdszelem8  35203  bj-fununsn1  37254  bj-fvsnun2  37257  poimirlem16  37643  osumcllem10N  39967  pexmidlem7N  39978  mapdindp2  41723  mapdindp3  41724  hdmapval3lemN  41839  hdmap11lem1  41843  fourierdlem80  46201
  Copyright terms: Public domain W3C validator