Theorem unisucs

Description: The union of the successor of a set is equal to the binary union of that set with its union. (Contributed by NM, 30-Aug-1993) Extract from unisuc . (Revised by BJ, 28-Dec-2024)

	Ref	Expression
Assertion	unisucs	$$⊢A\in V\to \bigcup \mathrm{suc}A=\bigcup A\cup A$$

Proof

Step	Hyp	Ref	Expression
1		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
2	1	unieqi	$$⊢\bigcup \mathrm{suc}A=\bigcup \left(A\cup \left\{A\right\}\right)$$
3	2	a1i	$$⊢A\in V\to \bigcup \mathrm{suc}A=\bigcup \left(A\cup \left\{A\right\}\right)$$
4		uniun	$$⊢\bigcup \left(A\cup \left\{A\right\}\right)=\bigcup A\cup \bigcup \left\{A\right\}$$
5	4	a1i	$$⊢A\in V\to \bigcup \left(A\cup \left\{A\right\}\right)=\bigcup A\cup \bigcup \left\{A\right\}$$
6		unisng	$$⊢A\in V\to \bigcup \left\{A\right\}=A$$
7	6	uneq2d	$$⊢A\in V\to \bigcup A\cup \bigcup \left\{A\right\}=\bigcup A\cup A$$
8	3 5 7	3eqtrd	$$⊢A\in V\to \bigcup \mathrm{suc}A=\bigcup A\cup A$$