Theorem uni0

Description: The union of the empty set is the empty set. Theorem 8.7 of Quine p. 54. (Contributed by NM, 16-Sep-1993) Remove use of ax-nul . (Revised by Eric Schmidt, 4-Apr-2007)

	Ref	Expression
Assertion	uni0	$$⊢\bigcup \varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq \left\{\varnothing \right\}$$
2		uni0b	$$⊢\bigcup \varnothing =\varnothing \leftrightarrow \varnothing \subseteq \left\{\varnothing \right\}$$
3	1 2	mpbir	$$⊢\bigcup \varnothing =\varnothing$$