Theorem iunsuc

Description: Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013) (Proof shortened by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Hypotheses	iunsuc.1	$$⊢A\in \mathrm{V}$$
	iunsuc.2	$$⊢x=A\to B=C$$
Assertion	iunsuc	$$⊢\bigcup _{x\in \mathrm{suc}A}B=\bigcup _{x\in A}B\cup C$$

Proof

Step	Hyp	Ref	Expression
1		iunsuc.1	$$⊢A\in \mathrm{V}$$
2		iunsuc.2	$$⊢x=A\to B=C$$
3		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
4		iuneq1	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}\to \bigcup _{x\in \mathrm{suc}A}B=\bigcup _{x\in A\cup \left\{A\right\}}B$$
5	3 4	ax-mp	$$⊢\bigcup _{x\in \mathrm{suc}A}B=\bigcup _{x\in A\cup \left\{A\right\}}B$$
6		iunxun	$$⊢\bigcup _{x\in A\cup \left\{A\right\}}B=\bigcup _{x\in A}B\cup \bigcup _{x\in \left\{A\right\}}B$$
7	1 2	iunxsn	$$⊢\bigcup _{x\in \left\{A\right\}}B=C$$
8	7	uneq2i	$$⊢\bigcup _{x\in A}B\cup \bigcup _{x\in \left\{A\right\}}B=\bigcup _{x\in A}B\cup C$$
9	5 6 8	3eqtri	$$⊢\bigcup _{x\in \mathrm{suc}A}B=\bigcup _{x\in A}B\cup C$$