Theorem ssneldd 3916

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  0nelrel0  5716  cantnfp1lem3  9711  fpwwe2lem12  10757  pwfseqlem3  10775  hashbclem  14627  sumrblem  15909  incexclem  16037  prodrblem  16128  fprodntriv  16141  ramub1lem2  17237  mreexmrid  17849  mreexexlem2d  17851  acsfiindd  18759  lbspss  21390  lbsextlem4  21472  ssdifidlprm  21675  lindfrn  22160  fclscmpi  24381  lhop2  26368  lhop  26369  dvcnvrelem1  26370  axlowdimlem17  29569  cyc3co2  33777  esplyind  34290  erdszelem8  36143  bj-fununsn1  38379  bj-fvsnun2  38382  poimirlem16  38759  osumcllem10N  41225  pexmidlem7N  41236  mapdindp2  42981  mapdindp3  42982  hdmapval3lemN  43097  hdmap11lem1  43101  fourierdlem80  47411