Theorem ssneldd 3911

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3896

This theorem is used by:  0nelrel0  5710  cantnfp1lem3  9684  fpwwe2lem12  10730  pwfseqlem3  10748  hashbclem  14600  sumrblem  15882  incexclem  16010  prodrblem  16101  fprodntriv  16114  ramub1lem2  17210  mreexmrid  17822  mreexexlem2d  17824  acsfiindd  18732  lbspss  21362  lbsextlem4  21444  ssdifidlprm  21647  lindfrn  22132  fclscmpi  24353  lhop2  26340  lhop  26341  dvcnvrelem1  26342  axlowdimlem17  29541  cyc3co2  33747  esplyind  34253  erdszelem8  36049  bj-fununsn1  38267  bj-fvsnun2  38270  poimirlem16  38647  osumcllem10N  41115  pexmidlem7N  41126  mapdindp2  42871  mapdindp3  42872  hdmapval3lemN  42987  hdmap11lem1  42991  fourierdlem80  47289