Theorem un00

Description: Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004)

	Ref	Expression
Assertion	un00	$$⊢\left(A=\varnothing \wedge B=\varnothing \right)\leftrightarrow A\cup B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		uneq12	$$⊢\left(A=\varnothing \wedge B=\varnothing \right)\to A\cup B=\varnothing \cup \varnothing$$
2		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
3	1 2	eqtrdi	$$⊢\left(A=\varnothing \wedge B=\varnothing \right)\to A\cup B=\varnothing$$
4		ssun1	$$⊢A\subseteq A\cup B$$
5		sseq2	$$⊢A\cup B=\varnothing \to \left(A\subseteq A\cup B\leftrightarrow A\subseteq \varnothing \right)$$
6	4 5	mpbii	$$⊢A\cup B=\varnothing \to A\subseteq \varnothing$$
7		ss0b	$$⊢A\subseteq \varnothing \leftrightarrow A=\varnothing$$
8	6 7	sylib	$$⊢A\cup B=\varnothing \to A=\varnothing$$
9		ssun2	$$⊢B\subseteq A\cup B$$
10		sseq2	$$⊢A\cup B=\varnothing \to \left(B\subseteq A\cup B\leftrightarrow B\subseteq \varnothing \right)$$
11	9 10	mpbii	$$⊢A\cup B=\varnothing \to B\subseteq \varnothing$$
12		ss0b	$$⊢B\subseteq \varnothing \leftrightarrow B=\varnothing$$
13	11 12	sylib	$$⊢A\cup B=\varnothing \to B=\varnothing$$
14	8 13	jca	$$⊢A\cup B=\varnothing \to \left(A=\varnothing \wedge B=\varnothing \right)$$
15	3 14	impbii	$$⊢\left(A=\varnothing \wedge B=\varnothing \right)\leftrightarrow A\cup B=\varnothing$$