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

Theorem ssneldd 3598
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 3597 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1988  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  0nelrel  5152  cantnfp1lem3  8562  fpwwe2lem13  9449  pwfseqlem3  9467  hashbclem  13219  sumrblem  14423  incexclem  14549  prodrblem  14640  fprodntriv  14653  ramub1lem2  15712  mreexmrid  16284  mreexexlem2d  16286  acsfiindd  17158  lbspss  19063  lbsextlem4  19142  lindfrn  20141  fclscmpi  21814  lhop2  23759  lhop  23760  dvcnvrelem1  23761  axlowdimlem17  25819  erdszelem8  31154  osumcllem10N  35070  pexmidlem7N  35081  mapdindp2  36829  mapdindp3  36830  hdmapval3lemN  36948  hdmap11lem1  36952  fourierdlem80  40166
  Copyright terms: Public domain W3C validator