Theorem ssneldd 3985

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  0nelrel0  5736  cantnfp1lem3  9677  fpwwe2lem12  10639  pwfseqlem3  10657  hashbclem  14415  sumrblem  15661  incexclem  15786  prodrblem  15877  fprodntriv  15890  ramub1lem2  16964  mreexmrid  17591  mreexexlem2d  17593  acsfiindd  18510  lbspss  20837  lbsextlem4  20919  lindfrn  21595  fclscmpi  23753  lhop2  25756  lhop  25757  dvcnvrelem1  25758  axlowdimlem17  28471  cyc3co2  32557  erdszelem8  34475  bj-fununsn1  36437  bj-fvsnun2  36440  poimirlem16  36807  osumcllem10N  39139  pexmidlem7N  39150  mapdindp2  40895  mapdindp3  40896  hdmapval3lemN  41011  hdmap11lem1  41015  fourierdlem80  45201