Theorem unidif0

Description: The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004) (Proof shortened by Eric Schmidt, 25-Apr-2026)

	Ref	Expression
Assertion	unidif0	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		undif1	$$⊢\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}=A\cup \left\{\varnothing \right\}$$
2	1	unieqi	$$⊢\bigcup \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)=\bigcup \left(A\cup \left\{\varnothing \right\}\right)$$
3		uniun	$$⊢\bigcup \left(A\cup \left\{\varnothing \right\}\right)=\bigcup A\cup \bigcup \left\{\varnothing \right\}$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	4	unisn	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$
6	5	uneq2i	$$⊢\bigcup A\cup \bigcup \left\{\varnothing \right\}=\bigcup A\cup \varnothing$$
7	2 3 6	3eqtri	$$⊢\bigcup \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)=\bigcup A\cup \varnothing$$
8		uniun	$$⊢\bigcup \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)=\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \bigcup \left\{\varnothing \right\}$$
9	5	uneq2i	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \bigcup \left\{\varnothing \right\}=\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \varnothing$$
10		un0	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \varnothing =\bigcup \left(A\setminus \left\{\varnothing \right\}\right)$$
11	8 9 10	3eqtri	$$⊢\bigcup \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)=\bigcup \left(A\setminus \left\{\varnothing \right\}\right)$$
12		un0	$$⊢\bigcup A\cup \varnothing =\bigcup A$$
13	7 11 12	3eqtr3i	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)=\bigcup A$$