Theorem ssneldd 3925

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3907

This theorem is referenced by:  0nelrel0  5684  cantnfp1lem3  9592  fpwwe2lem12  10556  pwfseqlem3  10574  hashbclem  14405  sumrblem  15664  incexclem  15792  prodrblem  15885  fprodntriv  15898  ramub1lem2  16989  mreexmrid  17600  mreexexlem2d  17602  acsfiindd  18510  lbspss  21069  lbsextlem4  21151  lindfrn  21811  fclscmpi  24004  lhop2  25992  lhop  25993  dvcnvrelem1  25994  axlowdimlem17  29041  cyc3co2  33216  ssdifidlprm  33533  esplyind  33734  erdszelem8  35396  bj-fununsn1  37583  bj-fvsnun2  37586  poimirlem16  37971  osumcllem10N  40425  pexmidlem7N  40436  mapdindp2  42181  mapdindp3  42182  hdmapval3lemN  42297  hdmap11lem1  42301  fourierdlem80  46632