Theorem ssneldd 3977

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2098   ⊆ wss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  0nelrel0  5726  cantnfp1lem3  9670  fpwwe2lem12  10632  pwfseqlem3  10650  hashbclem  14407  sumrblem  15653  incexclem  15778  prodrblem  15869  fprodntriv  15882  ramub1lem2  16956  mreexmrid  17583  mreexexlem2d  17585  acsfiindd  18505  lbspss  20915  lbsextlem4  20997  lindfrn  21676  fclscmpi  23843  lhop2  25858  lhop  25859  dvcnvrelem1  25860  axlowdimlem17  28640  cyc3co2  32726  erdszelem8  34644  bj-fununsn1  36590  bj-fvsnun2  36593  poimirlem16  36960  osumcllem10N  39292  pexmidlem7N  39303  mapdindp2  41048  mapdindp3  41049  hdmapval3lemN  41164  hdmap11lem1  41168  fourierdlem80  45353