Theorem ssneldd 3928

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  0nelrel0  5646  cantnfp1lem3  9399  fpwwe2lem12  10382  pwfseqlem3  10400  hashbclem  14145  sumrblem  15404  incexclem  15529  prodrblem  15620  fprodntriv  15633  ramub1lem2  16709  mreexmrid  17333  mreexexlem2d  17335  acsfiindd  18252  lbspss  20325  lbsextlem4  20404  lindfrn  21009  fclscmpi  23161  lhop2  25160  lhop  25161  dvcnvrelem1  25162  axlowdimlem17  27307  cyc3co2  31386  erdszelem8  33139  bj-fununsn1  35403  bj-fvsnun2  35406  poimirlem16  35772  osumcllem10N  37958  pexmidlem7N  37969  mapdindp2  39714  mapdindp3  39715  hdmapval3lemN  39830  hdmap11lem1  39834  fourierdlem80  43681