Theorem ssneldd 3970

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  0nelrel0  5607  cantnfp1lem3  9137  fpwwe2lem13  10058  pwfseqlem3  10076  hashbclem  13804  sumrblem  15062  incexclem  15185  prodrblem  15277  fprodntriv  15290  ramub1lem2  16357  mreexmrid  16908  mreexexlem2d  16910  acsfiindd  17781  lbspss  19848  lbsextlem4  19927  lindfrn  20959  fclscmpi  22631  lhop2  24606  lhop  24607  dvcnvrelem1  24608  axlowdimlem17  26738  cyc3co2  30777  erdszelem8  32440  bj-fununsn1  34529  bj-fvsnun2  34532  osumcllem10N  37095  pexmidlem7N  37106  mapdindp2  38851  mapdindp3  38852  hdmapval3lemN  38967  hdmap11lem1  38971  fourierdlem80  42464