Theorem ssneldd 3924

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

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

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 2811  df-ss 3906

This theorem is referenced by:  0nelrel0  5691  cantnfp1lem3  9601  fpwwe2lem12  10565  pwfseqlem3  10583  hashbclem  14414  sumrblem  15673  incexclem  15801  prodrblem  15894  fprodntriv  15907  ramub1lem2  16998  mreexmrid  17609  mreexexlem2d  17611  acsfiindd  18519  lbspss  21077  lbsextlem4  21159  lindfrn  21801  fclscmpi  23994  lhop2  25982  lhop  25983  dvcnvrelem1  25984  axlowdimlem17  29027  cyc3co2  33201  ssdifidlprm  33518  esplyind  33719  erdszelem8  35380  bj-fununsn1  37567  bj-fvsnun2  37570  poimirlem16  37957  osumcllem10N  40411  pexmidlem7N  40422  mapdindp2  42167  mapdindp3  42168  hdmapval3lemN  42283  hdmap11lem1  42287  fourierdlem80  46614