Theorem ssneldd 3942

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2145   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840  df-ss 3924

This theorem is referenced by:  0nelrel0  5712  cantnfp1lem3  9637  fpwwe2lem12  10615  pwfseqlem3  10633  hashbclem  14479  sumrblem  15752  incexclem  15880  prodrblem  15973  fprodntriv  15986  ramub1lem2  17077  mreexmrid  17689  mreexexlem2d  17691  acsfiindd  18599  lbspss  21172  lbsextlem4  21254  ssdifidlprm  21446  lindfrn  21931  fclscmpi  24147  lhop2  26135  lhop  26136  dvcnvrelem1  26137  axlowdimlem17  29217  cyc3co2  33373  esplyind  33882  erdszelem8  35561  bj-fununsn1  37757  bj-fvsnun2  37760  poimirlem16  38147  osumcllem10N  40601  pexmidlem7N  40612  mapdindp2  42357  mapdindp3  42358  hdmapval3lemN  42473  hdmap11lem1  42477  fourierdlem80  46758