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 15	1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3919

This theorem is referenced by:  0nelrel0  5676  cantnfp1lem3  9570  fpwwe2lem12  10533  pwfseqlem3  10551  hashbclem  14359  sumrblem  15618  incexclem  15743  prodrblem  15836  fprodntriv  15849  ramub1lem2  16939  mreexmrid  17549  mreexexlem2d  17551  acsfiindd  18459  lbspss  21017  lbsextlem4  21099  lindfrn  21759  fclscmpi  23945  lhop2  25948  lhop  25949  dvcnvrelem1  25950  axlowdimlem17  28937  cyc3co2  33107  ssdifidlprm  33421  erdszelem8  35240  bj-fununsn1  37293  bj-fvsnun2  37296  poimirlem16  37682  osumcllem10N  40010  pexmidlem7N  40021  mapdindp2  41766  mapdindp3  41767  hdmapval3lemN  41882  hdmap11lem1  41886  fourierdlem80  46230