Theorem ssneldd 4011

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

Step	Hyp	Ref	Expression
1		ssneldd.2	. 2 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵)
2		ssneld.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	2	ssneld 4010	. 2 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴))
4	1, 3	mpd 15	1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  0nelrel0  5760  cantnfp1lem3  9749  fpwwe2lem12  10711  pwfseqlem3  10729  hashbclem  14501  sumrblem  15759  incexclem  15884  prodrblem  15977  fprodntriv  15990  ramub1lem2  17074  mreexmrid  17701  mreexexlem2d  17703  acsfiindd  18623  lbspss  21104  lbsextlem4  21186  lindfrn  21864  fclscmpi  24058  lhop2  26074  lhop  26075  dvcnvrelem1  26076  axlowdimlem17  28991  cyc3co2  33133  ssdifidlprm  33451  erdszelem8  35166  bj-fununsn1  37219  bj-fvsnun2  37222  poimirlem16  37596  osumcllem10N  39922  pexmidlem7N  39933  mapdindp2  41678  mapdindp3  41679  hdmapval3lemN  41794  hdmap11lem1  41798  fourierdlem80  46107