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

Metamath Proof Explorer

Theorem pssne

Description: Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015)

		Ref	Expression
	Assertion	pssne	$⊢ A \subset B \to A \neq B$

Step	Hyp	Ref	Expression
1		df-pss	$⊢ A \subset B \leftrightarrow (A \subseteq B \land A \neq B)$
2	1	simprbi	$⊢ A \subset B \to A \neq B$