Theorem ssneldd 3933

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ⊆ wss 3898

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 2115

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

This theorem is referenced by:  0nelrel0  5679  cantnfp1lem3  9577  fpwwe2lem12  10540  pwfseqlem3  10558  hashbclem  14361  sumrblem  15620  incexclem  15745  prodrblem  15838  fprodntriv  15851  ramub1lem2  16941  mreexmrid  17551  mreexexlem2d  17553  acsfiindd  18461  lbspss  21018  lbsextlem4  21100  lindfrn  21760  fclscmpi  23945  lhop2  25948  lhop  25949  dvcnvrelem1  25950  axlowdimlem17  28938  cyc3co2  33116  ssdifidlprm  33430  esplyind  33613  erdszelem8  35263  bj-fununsn1  37318  bj-fvsnun2  37321  poimirlem16  37697  osumcllem10N  40085  pexmidlem7N  40096  mapdindp2  41841  mapdindp3  41842  hdmapval3lemN  41957  hdmap11lem1  41961  fourierdlem80  46309