Theorem ssneldd 3961

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809  df-ss 3943

This theorem is referenced by:  0nelrel0  5714  cantnfp1lem3  9694  fpwwe2lem12  10656  pwfseqlem3  10674  hashbclem  14470  sumrblem  15727  incexclem  15852  prodrblem  15945  fprodntriv  15958  ramub1lem2  17047  mreexmrid  17655  mreexexlem2d  17657  acsfiindd  18563  lbspss  21040  lbsextlem4  21122  lindfrn  21781  fclscmpi  23967  lhop2  25972  lhop  25973  dvcnvrelem1  25974  axlowdimlem17  28937  cyc3co2  33151  ssdifidlprm  33473  erdszelem8  35220  bj-fununsn1  37271  bj-fvsnun2  37274  poimirlem16  37660  osumcllem10N  39984  pexmidlem7N  39995  mapdindp2  41740  mapdindp3  41741  hdmapval3lemN  41856  hdmap11lem1  41860  fourierdlem80  46215