Theorem iunxunsn

Description: Appending a set to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Hypothesis	iunxunsn.1	$$⊢x=X\to B=C$$
Assertion	iunxunsn	$$⊢X\in V\to \bigcup _{x\in A\cup \left\{X\right\}}B=\bigcup _{x\in A}B\cup C$$

Proof

Step	Hyp	Ref	Expression
1		iunxunsn.1	$$⊢x=X\to B=C$$
2		iunxun	$$⊢\bigcup _{x\in A\cup \left\{X\right\}}B=\bigcup _{x\in A}B\cup \bigcup _{x\in \left\{X\right\}}B$$
3	1	iunxsng	$$⊢X\in V\to \bigcup _{x\in \left\{X\right\}}B=C$$
4	3	uneq2d	$$⊢X\in V\to \bigcup _{x\in A}B\cup \bigcup _{x\in \left\{X\right\}}B=\bigcup _{x\in A}B\cup C$$
5	2 4	eqtrid	$$⊢X\in V\to \bigcup _{x\in A\cup \left\{X\right\}}B=\bigcup _{x\in A}B\cup C$$