Theorem uni0c

Description: The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006)

	Ref	Expression
Assertion	uni0c	$$⊢\bigcup A=\varnothing \leftrightarrow \forall x\in Ax=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		uni0b	$$⊢\bigcup A=\varnothing \leftrightarrow A\subseteq \left\{\varnothing \right\}$$
2		dfss3	$$⊢A\subseteq \left\{\varnothing \right\}\leftrightarrow \forall x\in Ax\in \left\{\varnothing \right\}$$
3		velsn	$$⊢x\in \left\{\varnothing \right\}\leftrightarrow x=\varnothing$$
4	3	ralbii	$$⊢\forall x\in Ax\in \left\{\varnothing \right\}\leftrightarrow \forall x\in Ax=\varnothing$$
5	1 2 4	3bitri	$$⊢\bigcup A=\varnothing \leftrightarrow \forall x\in Ax=\varnothing$$