Theorem unidif0OLD

Description: Obsolete version of unidif0 as of 25-Apr-2026. (Contributed by NM, 22-Mar-2004) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2		undif1	$$⊢\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}=A\cup \left\{\varnothing \right\}$$
3		uncom	$$⊢A\cup \left\{\varnothing \right\}=\left\{\varnothing \right\}\cup A$$
4	2 3	eqtr2i	$$⊢\left\{\varnothing \right\}\cup A=\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$$
5	4	unieqi	$$⊢\bigcup \left(\left\{\varnothing \right\}\cup A\right)=\bigcup \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	6	unisn	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$
8	7	uneq2i	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \bigcup \left\{\varnothing \right\}=\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \varnothing$$
9		un0	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \varnothing =\bigcup \left(A\setminus \left\{\varnothing \right\}\right)$$
10	8 9	eqtr2i	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)=\bigcup \left(A\setminus \left\{\varnothing \right\}\right)\cup \bigcup \left\{\varnothing \right\}$$
11	1 5 10	3eqtr4ri	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)=\bigcup \left(\left\{\varnothing \right\}\cup A\right)$$
12		uniun	$$⊢\bigcup \left(\left\{\varnothing \right\}\cup A\right)=\bigcup \left\{\varnothing \right\}\cup \bigcup A$$
13	7	uneq1i	$$⊢\bigcup \left\{\varnothing \right\}\cup \bigcup A=\varnothing \cup \bigcup A$$
14	11 12 13	3eqtri	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)=\varnothing \cup \bigcup A$$
15		uncom	$$⊢\varnothing \cup \bigcup A=\bigcup A\cup \varnothing$$
16		un0	$$⊢\bigcup A\cup \varnothing =\bigcup A$$
17	14 15 16	3eqtri	$$⊢\bigcup \left(A\setminus \left\{\varnothing \right\}\right)=\bigcup A$$