Theorem ssneldd 3936

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-ss 3918

This theorem is referenced by:  0nelrel0  5684  cantnfp1lem3  9589  fpwwe2lem12  10553  pwfseqlem3  10571  hashbclem  14375  sumrblem  15634  incexclem  15759  prodrblem  15852  fprodntriv  15865  ramub1lem2  16955  mreexmrid  17566  mreexexlem2d  17568  acsfiindd  18476  lbspss  21034  lbsextlem4  21116  lindfrn  21776  fclscmpi  23973  lhop2  25976  lhop  25977  dvcnvrelem1  25978  axlowdimlem17  29031  cyc3co2  33222  ssdifidlprm  33539  esplyind  33731  erdszelem8  35392  bj-fununsn1  37458  bj-fvsnun2  37461  poimirlem16  37837  osumcllem10N  40225  pexmidlem7N  40236  mapdindp2  41981  mapdindp3  41982  hdmapval3lemN  42097  hdmap11lem1  42101  fourierdlem80  46430