Theorem ssneldd 3940

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

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

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 2803  df-ss 3922

This theorem is referenced by:  0nelrel0  5683  cantnfp1lem3  9595  fpwwe2lem12  10555  pwfseqlem3  10573  hashbclem  14377  sumrblem  15636  incexclem  15761  prodrblem  15854  fprodntriv  15867  ramub1lem2  16957  mreexmrid  17567  mreexexlem2d  17569  acsfiindd  18477  lbspss  21004  lbsextlem4  21086  lindfrn  21746  fclscmpi  23932  lhop2  25936  lhop  25937  dvcnvrelem1  25938  axlowdimlem17  28921  cyc3co2  33095  ssdifidlprm  33405  erdszelem8  35170  bj-fununsn1  37226  bj-fvsnun2  37229  poimirlem16  37615  osumcllem10N  39944  pexmidlem7N  39955  mapdindp2  41700  mapdindp3  41701  hdmapval3lemN  41816  hdmap11lem1  41820  fourierdlem80  46168