Theorem ssneldd 3943

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2841  df-ss 3925

This theorem is used by:  0nelrel0  5726  cantnfp1lem3  9659  fpwwe2lem12  10645  pwfseqlem3  10663  hashbclem  14509  sumrblem  15788  incexclem  15916  prodrblem  16009  fprodntriv  16022  ramub1lem2  17112  mreexmrid  17724  mreexexlem2d  17726  acsfiindd  18634  lbspss  21240  lbsextlem4  21322  ssdifidlprm  21523  lindfrn  22008  fclscmpi  24223  lhop2  26211  lhop  26212  dvcnvrelem1  26213  axlowdimlem17  29345  cyc3co2  33491  esplyind  33996  erdszelem8  35711  bj-fununsn1  37938  bj-fvsnun2  37941  poimirlem16  38328  osumcllem10N  40780  pexmidlem7N  40791  mapdindp2  42536  mapdindp3  42537  hdmapval3lemN  42652  hdmap11lem1  42656  fourierdlem80  46941