Theorem uni0b

Description: The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004)

	Ref	Expression
Assertion	uni0b	$$⊢\bigcup A=\varnothing \leftrightarrow A\subseteq \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		velsn	$$⊢x\in \left\{\varnothing \right\}\leftrightarrow x=\varnothing$$
2	1	ralbii	$$⊢\forall x\in Ax\in \left\{\varnothing \right\}\leftrightarrow \forall x\in Ax=\varnothing$$
3		dfss3	$$⊢A\subseteq \left\{\varnothing \right\}\leftrightarrow \forall x\in Ax\in \left\{\varnothing \right\}$$
4		neq0	$$⊢\neg \bigcup A=\varnothing \leftrightarrow \exists yy\in \bigcup A$$
5		rexcom4	$$⊢\exists x\in A\exists yy\in x\leftrightarrow \exists y\exists x\in Ay\in x$$
6		neq0	$$⊢\neg x=\varnothing \leftrightarrow \exists yy\in x$$
7	6	rexbii	$$⊢\exists x\in A\neg x=\varnothing \leftrightarrow \exists x\in A\exists yy\in x$$
8		eluni2	$$⊢y\in \bigcup A\leftrightarrow \exists x\in Ay\in x$$
9	8	exbii	$$⊢\exists yy\in \bigcup A\leftrightarrow \exists y\exists x\in Ay\in x$$
10	5 7 9	3bitr4ri	$$⊢\exists yy\in \bigcup A\leftrightarrow \exists x\in A\neg x=\varnothing$$
11		rexnal	$$⊢\exists x\in A\neg x=\varnothing \leftrightarrow \neg \forall x\in Ax=\varnothing$$
12	4 10 11	3bitri	$$⊢\neg \bigcup A=\varnothing \leftrightarrow \neg \forall x\in Ax=\varnothing$$
13	12	con4bii	$$⊢\bigcup A=\varnothing \leftrightarrow \forall x\in Ax=\varnothing$$
14	2 3 13	3bitr4ri	$$⊢\bigcup A=\varnothing \leftrightarrow A\subseteq \left\{\varnothing \right\}$$