Theorem ssneld 3940

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 3937	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	2	con3d 153	1 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923

This theorem is referenced by:  ssneldd  3941  kmlem2  10136  hashbclem  14491  prodss  16003  coprmproddvdslem  16721  mrissmrid  17698  mpfrcl  22217  onsuct0  36933  ftc1anc  38333  dvhdimlem  42199  dvh3dim2  42203  dvh3dim3N  42204  mapdh9a  42544  hdmapval0  42588  hdmap11lem2  42597  iundjiunlem  47156  elbigolo1  49320