Theorem ssneldd 3939

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2141   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3921

This theorem is referenced by:  0nelrel0  5705  cantnfp1lem3  9632  fpwwe2lem12  10597  pwfseqlem3  10615  hashbclem  14462  sumrblem  15721  incexclem  15849  prodrblem  15942  fprodntriv  15955  ramub1lem2  17046  mreexmrid  17658  mreexexlem2d  17660  acsfiindd  18568  lbspss  21129  lbsextlem4  21211  lindfrn  21853  fclscmpi  24069  lhop2  26057  lhop  26058  dvcnvrelem1  26059  axlowdimlem17  29105  cyc3co2  33281  ssdifidlprm  33606  esplyind  33833  erdszelem8  35512  bj-fununsn1  37709  bj-fvsnun2  37712  poimirlem16  38099  osumcllem10N  40553  pexmidlem7N  40564  mapdindp2  42309  mapdindp3  42310  hdmapval3lemN  42425  hdmap11lem1  42429  fourierdlem80  46724