Theorem nsspssun

Description: Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004)

	Ref	Expression
Assertion	nsspssun	$$⊢\neg A\subseteq B\leftrightarrow B\subset A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		ssun2	$$⊢B\subseteq A\cup B$$
2	1	biantrur	$$⊢\neg A\cup B\subseteq B\leftrightarrow \left(B\subseteq A\cup B\wedge \neg A\cup B\subseteq B\right)$$
3		ssid	$$⊢B\subseteq B$$
4	3	biantru	$$⊢A\subseteq B\leftrightarrow \left(A\subseteq B\wedge B\subseteq B\right)$$
5		unss	$$⊢\left(A\subseteq B\wedge B\subseteq B\right)\leftrightarrow A\cup B\subseteq B$$
6	4 5	bitri	$$⊢A\subseteq B\leftrightarrow A\cup B\subseteq B$$
7	2 6	xchnxbir	$$⊢\neg A\subseteq B\leftrightarrow \left(B\subseteq A\cup B\wedge \neg A\cup B\subseteq B\right)$$
8		dfpss3	$$⊢B\subset A\cup B\leftrightarrow \left(B\subseteq A\cup B\wedge \neg A\cup B\subseteq B\right)$$
9	7 8	bitr4i	$$⊢\neg A\subseteq B\leftrightarrow B\subset A\cup B$$