Theorem ssneld 3960

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809  df-ss 3943

This theorem is referenced by:  ssneldd  3961  kmlem2  10166  hashbclem  14470  prodss  15963  coprmproddvdslem  16681  mrissmrid  17653  mpfrcl  22043  onsuct0  36459  ftc1anc  37725  dvhdimlem  41463  dvh3dim2  41467  dvh3dim3N  41468  mapdh9a  41808  hdmapval0  41852  hdmap11lem2  41861  iundjiunlem  46488  elbigolo1  48537