Theorem ssneldd 3929

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2104   ⊆ wss 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  0nelrel0  5658  cantnfp1lem3  9482  fpwwe2lem12  10444  pwfseqlem3  10462  hashbclem  14209  sumrblem  15468  incexclem  15593  prodrblem  15684  fprodntriv  15697  ramub1lem2  16773  mreexmrid  17397  mreexexlem2d  17399  acsfiindd  18316  lbspss  20389  lbsextlem4  20468  lindfrn  21073  fclscmpi  23225  lhop2  25224  lhop  25225  dvcnvrelem1  25226  axlowdimlem17  27371  cyc3co2  31452  erdszelem8  33205  bj-fununsn1  35468  bj-fvsnun2  35471  poimirlem16  35837  osumcllem10N  38021  pexmidlem7N  38032  mapdindp2  39777  mapdindp3  39778  hdmapval3lemN  39893  hdmap11lem1  39897  fourierdlem80  43776