Theorem ssneldd 3904

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  0nelrel0  5609  cantnfp1lem3  9295  fpwwe2lem12  10256  pwfseqlem3  10274  hashbclem  14016  sumrblem  15275  incexclem  15400  prodrblem  15491  fprodntriv  15504  ramub1lem2  16580  mreexmrid  17146  mreexexlem2d  17148  acsfiindd  18059  lbspss  20119  lbsextlem4  20198  lindfrn  20783  fclscmpi  22926  lhop2  24912  lhop  24913  dvcnvrelem1  24914  axlowdimlem17  27049  cyc3co2  31126  erdszelem8  32873  bj-fununsn1  35159  bj-fvsnun2  35162  poimirlem16  35530  osumcllem10N  37716  pexmidlem7N  37727  mapdindp2  39472  mapdindp3  39473  hdmapval3lemN  39588  hdmap11lem1  39592  fourierdlem80  43402