Theorem ssneldd 3938

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920

This theorem is referenced by:  0nelrel0  5692  cantnfp1lem3  9601  fpwwe2lem12  10565  pwfseqlem3  10583  hashbclem  14387  sumrblem  15646  incexclem  15771  prodrblem  15864  fprodntriv  15877  ramub1lem2  16967  mreexmrid  17578  mreexexlem2d  17580  acsfiindd  18488  lbspss  21046  lbsextlem4  21128  lindfrn  21788  fclscmpi  23985  lhop2  25988  lhop  25989  dvcnvrelem1  25990  axlowdimlem17  29043  cyc3co2  33233  ssdifidlprm  33550  esplyind  33751  erdszelem8  35411  bj-fununsn1  37505  bj-fvsnun2  37508  poimirlem16  37884  osumcllem10N  40338  pexmidlem7N  40349  mapdindp2  42094  mapdindp3  42095  hdmapval3lemN  42210  hdmap11lem1  42214  fourierdlem80  46541