Theorem ssneld 3933

Description: If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ssneld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssneld	⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴))

Proof of Theorem ssneld

Step	Hyp	Ref	Expression
1		ssneld.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2	1	sseld 3930	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	2	con3d 153	1 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2835  df-ss 3916

This theorem is used by:  ssneldd  3934  kmlem2  10154  hashbclem  14517  prodss  16034  coprmproddvdslem  16752  mrissmrid  17729  mpfrcl  22301  onsuct0  37060  ftc1anc  38450  dvhdimlem  42317  dvh3dim2  42321  dvh3dim3N  42322  mapdh9a  42662  hdmapval0  42706  hdmap11lem2  42715  iundjiunlem  47287  elbigolo1  49487