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

Metamath Proof Explorer

Theorem pssdifn0

Description: A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994)

		Ref	Expression
	Assertion	pssdifn0	$⊢ (A \subseteq B \land A \neq B) \to B ∖ A \neq \emptyset$

Step	Hyp	Ref	Expression
1		ssdif0	$⊢ B \subseteq A \leftrightarrow B ∖ A = \emptyset$
2		eqss	$⊢ A = B \leftrightarrow (A \subseteq B \land B \subseteq A)$
3	2	simplbi2	$⊢ A \subseteq B \to (B \subseteq A \to A = B)$
4	1 3	biimtrrid	$⊢ A \subseteq B \to (B ∖ A = \emptyset \to A = B)$
5	4	necon3d	$⊢ A \subseteq B \to (A \neq B \to B ∖ A \neq \emptyset)$
6	5	imp	$⊢ (A \subseteq B \land A \neq B) \to B ∖ A \neq \emptyset$