Theorem ssneldd 3952

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804  df-ss 3934

This theorem is referenced by:  0nelrel0  5701  cantnfp1lem3  9640  fpwwe2lem12  10602  pwfseqlem3  10620  hashbclem  14424  sumrblem  15684  incexclem  15809  prodrblem  15902  fprodntriv  15915  ramub1lem2  17005  mreexmrid  17611  mreexexlem2d  17613  acsfiindd  18519  lbspss  20996  lbsextlem4  21078  lindfrn  21737  fclscmpi  23923  lhop2  25927  lhop  25928  dvcnvrelem1  25929  axlowdimlem17  28892  cyc3co2  33104  ssdifidlprm  33436  erdszelem8  35192  bj-fununsn1  37248  bj-fvsnun2  37251  poimirlem16  37637  osumcllem10N  39966  pexmidlem7N  39977  mapdindp2  41722  mapdindp3  41723  hdmapval3lemN  41838  hdmap11lem1  41842  fourierdlem80  46191