Theorem ssneld 3947

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-ss 3930

This theorem is referenced by:  ssneldd  3948  kmlem2  10131  hashbclem  14485  prodss  15997  coprmproddvdslem  16716  mrissmrid  17693  mpfrcl  22201  onsuct0  36837  ftc1anc  38235  dvhdimlem  42103  dvh3dim2  42107  dvh3dim3N  42108  mapdh9a  42448  hdmapval0  42492  hdmap11lem2  42501  iundjiunlem  47058  elbigolo1  49215