Theorem ssneldd 3941

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923

This theorem is referenced by:  0nelrel0  5723  cantnfp1lem3  9650  fpwwe2lem12  10628  pwfseqlem3  10646  hashbclem  14491  sumrblem  15764  incexclem  15892  prodrblem  15985  fprodntriv  15998  ramub1lem2  17088  mreexmrid  17700  mreexexlem2d  17702  acsfiindd  18610  lbspss  21184  lbsextlem4  21266  ssdifidlprm  21467  lindfrn  21952  fclscmpi  24167  lhop2  26155  lhop  26156  dvcnvrelem1  26157  axlowdimlem17  29286  cyc3co2  33438  esplyind  33943  erdszelem8  35668  bj-fununsn1  37875  bj-fvsnun2  37878  poimirlem16  38265  osumcllem10N  40717  pexmidlem7N  40728  mapdindp2  42473  mapdindp3  42474  hdmapval3lemN  42589  hdmap11lem1  42593  fourierdlem80  46880