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 2114   ⊆ wss 3890

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 3907

This theorem is referenced by:  0nelrel0  5682  cantnfp1lem3  9590  fpwwe2lem12  10554  pwfseqlem3  10572  hashbclem  14403  sumrblem  15662  incexclem  15790  prodrblem  15883  fprodntriv  15896  ramub1lem2  16987  mreexmrid  17598  mreexexlem2d  17600  acsfiindd  18508  lbspss  21067  lbsextlem4  21149  lindfrn  21809  fclscmpi  24003  lhop2  25992  lhop  25993  dvcnvrelem1  25994  axlowdimlem17  29046  cyc3co2  33221  ssdifidlprm  33538  esplyind  33739  erdszelem8  35401  bj-fununsn1  37580  bj-fvsnun2  37583  poimirlem16  37968  osumcllem10N  40422  pexmidlem7N  40433  mapdindp2  42178  mapdindp3  42179  hdmapval3lemN  42294  hdmap11lem1  42298  fourierdlem80  46629