Theorem ssneldd 3934

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

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

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 2147

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

This theorem is used by:  0nelrel0  5711  cantnfp1lem3  9665  fpwwe2lem12  10708  pwfseqlem3  10726  hashbclem  14577  sumrblem  15857  incexclem  15985  prodrblem  16076  fprodntriv  16089  ramub1lem2  17185  mreexmrid  17797  mreexexlem2d  17799  acsfiindd  18707  lbspss  21337  lbsextlem4  21419  ssdifidlprm  21622  lindfrn  22107  fclscmpi  24328  lhop2  26315  lhop  26316  dvcnvrelem1  26317  axlowdimlem17  29518  cyc3co2  33683  esplyind  34189  erdszelem8  35932  bj-fununsn1  38142  bj-fvsnun2  38145  poimirlem16  38522  osumcllem10N  40990  pexmidlem7N  41001  mapdindp2  42746  mapdindp3  42747  hdmapval3lemN  42862  hdmap11lem1  42866  fourierdlem80  47140