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

Metamath Proof Explorer

Theorem nssinpss

Description: Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	nssinpss	$⊢ \neg A \subseteq B \leftrightarrow A \cap B \subset A$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ A \cap B \subseteq A$
2	1	biantrur	$⊢ A \cap B \neq A \leftrightarrow (A \cap B \subseteq A \land A \cap B \neq A)$
3		dfss2	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
4	3	necon3bbii	$⊢ \neg A \subseteq B \leftrightarrow A \cap B \neq A$
5		df-pss	$⊢ A \cap B \subset A \leftrightarrow (A \cap B \subseteq A \land A \cap B \neq A)$
6	2 4 5	3bitr4i	$⊢ \neg A \subseteq B \leftrightarrow A \cap B \subset A$