Theorem ssneldd 3986

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968

This theorem is referenced by:  0nelrel0  5745  cantnfp1lem3  9720  fpwwe2lem12  10682  pwfseqlem3  10700  hashbclem  14491  sumrblem  15747  incexclem  15872  prodrblem  15965  fprodntriv  15978  ramub1lem2  17065  mreexmrid  17686  mreexexlem2d  17688  acsfiindd  18598  lbspss  21081  lbsextlem4  21163  lindfrn  21841  fclscmpi  24037  lhop2  26054  lhop  26055  dvcnvrelem1  26056  axlowdimlem17  28973  cyc3co2  33160  ssdifidlprm  33486  erdszelem8  35203  bj-fununsn1  37254  bj-fvsnun2  37257  poimirlem16  37643  osumcllem10N  39967  pexmidlem7N  39978  mapdindp2  41723  mapdindp3  41724  hdmapval3lemN  41839  hdmap11lem1  41843  fourierdlem80  46201