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

Theorem ssneldd 3639
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 3638 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  0nelrel  5196  cantnfp1lem3  8615  fpwwe2lem13  9502  pwfseqlem3  9520  hashbclem  13274  sumrblem  14486  incexclem  14612  prodrblem  14703  fprodntriv  14716  ramub1lem2  15778  mreexmrid  16350  mreexexlem2d  16352  acsfiindd  17224  lbspss  19130  lbsextlem4  19209  lindfrn  20208  fclscmpi  21880  lhop2  23823  lhop  23824  dvcnvrelem1  23825  axlowdimlem17  25883  erdszelem8  31306  osumcllem10N  35569  pexmidlem7N  35580  mapdindp2  37327  mapdindp3  37328  hdmapval3lemN  37446  hdmap11lem1  37450  fourierdlem80  40721
  Copyright terms: Public domain W3C validator