Theorem ssneldd 3854

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2051   ⊆ wss 3822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-in 3829  df-ss 3836

This theorem is referenced by:  0nelrel0  5458  cantnfp1lem3  8935  fpwwe2lem13  9860  pwfseqlem3  9878  hashbclem  13621  sumrblem  14926  incexclem  15049  prodrblem  15141  fprodntriv  15154  ramub1lem2  16217  mreexmrid  16784  mreexexlem2d  16786  acsfiindd  17657  lbspss  19588  lbsextlem4  19667  lindfrn  20682  fclscmpi  22356  lhop2  24330  lhop  24331  dvcnvrelem1  24332  axlowdimlem17  26462  cyc3co2  30491  erdszelem8  32067  bj-fununsn1  34041  bj-fvsnun2  34044  osumcllem10N  36583  pexmidlem7N  36594  mapdindp2  38339  mapdindp3  38340  hdmapval3lemN  38455  hdmap11lem1  38459  fourierdlem80  41936