Theorem pssdif 4319

Description: A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.)

Assertion

Ref	Expression
pssdif	⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)

Proof of Theorem pssdif

Step	Hyp	Ref	Expression
1		df-pss 3922	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		pssdifn0 4318	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∖ 𝐴) ≠ ∅)
3	1, 2	sylbi 219	1 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 399   ≠ wne 2956   ∖ cdif 3899   ⊆ wss 3902   ⊊ wpss 3903  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3455  df-dif 3905  df-ss 3919  df-pss 3922  df-nul 4284

This theorem is referenced by:  pssnel  4422  pgpfac1lem5  20112  fundmpss  36078  dfon2lem6  36097