Theorem ssneldd 3997

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979

This theorem is referenced by:  0nelrel0  5748  cantnfp1lem3  9717  fpwwe2lem12  10679  pwfseqlem3  10697  hashbclem  14487  sumrblem  15743  incexclem  15868  prodrblem  15961  fprodntriv  15974  ramub1lem2  17060  mreexmrid  17687  mreexexlem2d  17689  acsfiindd  18610  lbspss  21098  lbsextlem4  21180  lindfrn  21858  fclscmpi  24052  lhop2  26068  lhop  26069  dvcnvrelem1  26070  axlowdimlem17  28987  cyc3co2  33142  ssdifidlprm  33465  erdszelem8  35182  bj-fununsn1  37235  bj-fvsnun2  37238  poimirlem16  37622  osumcllem10N  39947  pexmidlem7N  39958  mapdindp2  41703  mapdindp3  41704  hdmapval3lemN  41819  hdmap11lem1  41823  fourierdlem80  46141