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

Metamath Proof Explorer

Theorem pssnssi

Description: A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypothesis	pssnssi.1	$⊢ A \subset B$
	Assertion	pssnssi	$⊢ \neg B \subseteq A$

Step	Hyp	Ref	Expression
1		pssnssi.1	$⊢ A \subset B$
2		dfpss3	$⊢ A \subset B \leftrightarrow (A \subseteq B \land \neg B \subseteq A)$
3	1 2	mpbi	$⊢ (A \subseteq B \land \neg B \subseteq A)$
4	3	simpri	$⊢ \neg B \subseteq A$