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

Metamath Proof Explorer

Theorem npss

Description: A class is not a proper subclass of another iff it satisfies a one-directional form of eqss . (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	npss	$⊢ \neg A \subset B \leftrightarrow (A \subseteq B \to A = B)$

Proof

Step	Hyp	Ref	Expression
1		pm4.61	$⊢ \neg (A \subseteq B \to A = B) \leftrightarrow (A \subseteq B \land \neg A = B)$
2		dfpss2	$⊢ A \subset B \leftrightarrow (A \subseteq B \land \neg A = B)$
3	1 2	bitr4i	$⊢ \neg (A \subseteq B \to A = B) \leftrightarrow A \subset B$
4	3	con1bii	$⊢ \neg A \subset B \leftrightarrow (A \subseteq B \to A = B)$