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) Avoid ax-11 . (Revised by TM, 1-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg y\in \varnothing$$
2	1	intnan	$$⊢\neg \left(x\in y\wedge y\in \varnothing \right)$$
3	2	nex	$$⊢\neg \exists y\left(x\in y\wedge y\in \varnothing \right)$$
4		eluni	$$⊢x\in \bigcup \varnothing \leftrightarrow \exists y\left(x\in y\wedge y\in \varnothing \right)$$
5	3 4	mtbir	$$⊢\neg x\in \bigcup \varnothing$$
6	5	nel0	$$⊢\bigcup \varnothing =\varnothing$$