Theorem ssneldd 3639

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2030   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621

This theorem is referenced by:  0nelrel  5196  cantnfp1lem3  8615  fpwwe2lem13  9502  pwfseqlem3  9520  hashbclem  13274  sumrblem  14486  incexclem  14612  prodrblem  14703  fprodntriv  14716  ramub1lem2  15778  mreexmrid  16350  mreexexlem2d  16352  acsfiindd  17224  lbspss  19130  lbsextlem4  19209  lindfrn  20208  fclscmpi  21880  lhop2  23823  lhop  23824  dvcnvrelem1  23825  axlowdimlem17  25883  erdszelem8  31306  osumcllem10N  35569  pexmidlem7N  35580  mapdindp2  37327  mapdindp3  37328  hdmapval3lemN  37446  hdmap11lem1  37450  fourierdlem80  40721