Theorem ssneldd 3925

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815  df-ss 3907

This theorem is referenced by:  0nelrel0  5685  cantnfp1lem3  9599  fpwwe2lem12  10563  pwfseqlem3  10581  hashbclem  14412  sumrblem  15671  incexclem  15799  prodrblem  15892  fprodntriv  15905  ramub1lem2  16996  mreexmrid  17607  mreexexlem2d  17609  acsfiindd  18517  lbspss  21079  lbsextlem4  21161  lindfrn  21803  fclscmpi  24019  lhop2  26007  lhop  26008  dvcnvrelem1  26009  axlowdimlem17  29052  cyc3co2  33228  ssdifidlprm  33548  esplyind  33766  erdszelem8  35433  bj-fununsn1  37620  bj-fvsnun2  37623  poimirlem16  38010  osumcllem10N  40464  pexmidlem7N  40475  mapdindp2  42220  mapdindp3  42221  hdmapval3lemN  42336  hdmap11lem1  42340  fourierdlem80  46636