Theorem ssneldd 3966

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 3965	. 2 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴))
4	1, 3	mpd 15	1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2808  df-ss 3948

This theorem is referenced by:  0nelrel0  5725  cantnfp1lem3  9702  fpwwe2lem12  10664  pwfseqlem3  10682  hashbclem  14473  sumrblem  15729  incexclem  15854  prodrblem  15947  fprodntriv  15960  ramub1lem2  17047  mreexmrid  17657  mreexexlem2d  17659  acsfiindd  18567  lbspss  21049  lbsextlem4  21131  lindfrn  21795  fclscmpi  23983  lhop2  25990  lhop  25991  dvcnvrelem1  25992  axlowdimlem17  28903  cyc3co2  33099  ssdifidlprm  33421  erdszelem8  35162  bj-fununsn1  37213  bj-fvsnun2  37216  poimirlem16  37602  osumcllem10N  39926  pexmidlem7N  39937  mapdindp2  41682  mapdindp3  41683  hdmapval3lemN  41798  hdmap11lem1  41802  fourierdlem80  46158