Theorem ssneldd 3984

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

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

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 3954  df-ss 3964

This theorem is referenced by:  0nelrel0  5734  cantnfp1lem3  9671  fpwwe2lem12  10633  pwfseqlem3  10651  hashbclem  14407  sumrblem  15653  incexclem  15778  prodrblem  15869  fprodntriv  15882  ramub1lem2  16956  mreexmrid  17583  mreexexlem2d  17585  acsfiindd  18502  lbspss  20685  lbsextlem4  20766  lindfrn  21367  fclscmpi  23524  lhop2  25523  lhop  25524  dvcnvrelem1  25525  axlowdimlem17  28205  cyc3co2  32286  erdszelem8  34177  bj-fununsn1  36122  bj-fvsnun2  36125  poimirlem16  36492  osumcllem10N  38824  pexmidlem7N  38835  mapdindp2  40580  mapdindp3  40581  hdmapval3lemN  40696  hdmap11lem1  40700  fourierdlem80  44888