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 2836  df-ss 3916

This theorem is used by:  ssneldd  3934  kmlem2  10223  hashbclem  14590  prodss  16107  coprmproddvdslem  16830  mrissmrid  17808  mpfrcl  22387  onsuct0  37209  ftc1anc  38599  dvhdimlem  42481  dvh3dim2  42485  dvh3dim3N  42486  mapdh9a  42826  hdmapval0  42870  hdmap11lem2  42879  iundjiunlem  47438  elbigolo1  49638