This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pssdif

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

		Ref	Expression
	Assertion	pssdif	$⊢ A \subset B \to B ∖ A \neq \emptyset$

Step	Hyp	Ref	Expression
1		df-pss	$⊢ A \subset B \leftrightarrow (A \subseteq B \land A \neq B)$
2		pssdifn0	$⊢ (A \subseteq B \land A \neq B) \to B ∖ A \neq \emptyset$
3	1 2	sylbi	$⊢ A \subset B \to B ∖ A \neq \emptyset$