Theorem ssneldd 3949

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3931

This theorem is referenced by:  0nelrel0  5698  cantnfp1lem3  9633  fpwwe2lem12  10595  pwfseqlem3  10613  hashbclem  14417  sumrblem  15677  incexclem  15802  prodrblem  15895  fprodntriv  15908  ramub1lem2  16998  mreexmrid  17604  mreexexlem2d  17606  acsfiindd  18512  lbspss  20989  lbsextlem4  21071  lindfrn  21730  fclscmpi  23916  lhop2  25920  lhop  25921  dvcnvrelem1  25922  axlowdimlem17  28885  cyc3co2  33097  ssdifidlprm  33429  erdszelem8  35185  bj-fununsn1  37241  bj-fvsnun2  37244  poimirlem16  37630  osumcllem10N  39959  pexmidlem7N  39970  mapdindp2  41715  mapdindp3  41716  hdmapval3lemN  41831  hdmap11lem1  41835  fourierdlem80  46184