Theorem disjpss

Description: A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004)

	Ref	Expression
Assertion	disjpss	$$⊢\left(A\cap B=\varnothing \wedge B\ne \varnothing \right)\to A\subset A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢B\subseteq B$$
2	1	biantru	$$⊢B\subseteq A\leftrightarrow \left(B\subseteq A\wedge B\subseteq B\right)$$
3		ssin	$$⊢\left(B\subseteq A\wedge B\subseteq B\right)\leftrightarrow B\subseteq A\cap B$$
4	2 3	bitri	$$⊢B\subseteq A\leftrightarrow B\subseteq A\cap B$$
5		sseq2	$$⊢A\cap B=\varnothing \to \left(B\subseteq A\cap B\leftrightarrow B\subseteq \varnothing \right)$$
6	4 5	bitrid	$$⊢A\cap B=\varnothing \to \left(B\subseteq A\leftrightarrow B\subseteq \varnothing \right)$$
7		ss0	$$⊢B\subseteq \varnothing \to B=\varnothing$$
8	6 7	biimtrdi	$$⊢A\cap B=\varnothing \to \left(B\subseteq A\to B=\varnothing \right)$$
9	8	necon3ad	$$⊢A\cap B=\varnothing \to \left(B\ne \varnothing \to \neg B\subseteq A\right)$$
10	9	imp	$$⊢\left(A\cap B=\varnothing \wedge B\ne \varnothing \right)\to \neg B\subseteq A$$
11		nsspssun	$$⊢\neg B\subseteq A\leftrightarrow A\subset B\cup A$$
12		uncom	$$⊢B\cup A=A\cup B$$
13	12	psseq2i	$$⊢A\subset B\cup A\leftrightarrow A\subset A\cup B$$
14	11 13	bitri	$$⊢\neg B\subseteq A\leftrightarrow A\subset A\cup B$$
15	10 14	sylib	$$⊢\left(A\cap B=\varnothing \wedge B\ne \varnothing \right)\to A\subset A\cup B$$