Theorem ssneldd 3937

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

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

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 2837  df-ss 3919

This theorem is used by:  0nelrel0  5719  cantnfp1lem3  9663  fpwwe2lem12  10655  pwfseqlem3  10673  hashbclem  14521  sumrblem  15801  incexclem  15929  prodrblem  16022  fprodntriv  16035  ramub1lem2  17125  mreexmrid  17737  mreexexlem2d  17739  acsfiindd  18647  lbspss  21272  lbsextlem4  21354  ssdifidlprm  21555  lindfrn  22040  fclscmpi  24261  lhop2  26249  lhop  26250  dvcnvrelem1  26251  axlowdimlem17  29423  cyc3co2  33588  esplyind  34093  erdszelem8  35785  bj-fununsn1  38013  bj-fvsnun2  38016  poimirlem16  38393  osumcllem10N  40846  pexmidlem7N  40857  mapdindp2  42602  mapdindp3  42603  hdmapval3lemN  42718  hdmap11lem1  42722  fourierdlem80  47022