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

Theorem ssneldd 3571
 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 3570 . 2 (𝜑 → (¬ 𝐶𝐵 → ¬ 𝐶𝐴))
41, 3mpd 15 1 (𝜑 → ¬ 𝐶𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1977   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554 This theorem is referenced by:  cantnfp1lem3  8460  fpwwe2lem13  9343  pwfseqlem3  9361  hashbclem  13093  sumrblem  14289  incexclem  14407  prodrblem  14498  fprodntriv  14511  ramub1lem2  15569  mreexmrid  16126  mreexexlem2d  16128  acsfiindd  17000  lbspss  18903  lbsextlem4  18982  lindfrn  19979  fclscmpi  21643  lhop2  23582  lhop  23583  dvcnvrelem1  23584  axlowdimlem17  25638  erdszelem8  30434  osumcllem10N  34269  pexmidlem7N  34280  mapdindp2  36028  mapdindp3  36029  hdmapval3lemN  36147  hdmap11lem1  36151  fourierdlem80  39079
 Copyright terms: Public domain W3C validator