Theorem iunxunpr

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

	Ref	Expression
Hypotheses	iunxunsn.1	$$⊢x=X\to B=C$$
	iunxunpr.2	$$⊢x=Y\to B=D$$
Assertion	iunxunpr	$$⊢\left(X\in V\wedge Y\in W\right)\to \bigcup _{x\in A\cup \left\{X,Y\right\}}B=\bigcup _{x\in A}B\cup \left(C\cup D\right)$$

Proof

Step	Hyp	Ref	Expression
1		iunxunsn.1	$$⊢x=X\to B=C$$
2		iunxunpr.2	$$⊢x=Y\to B=D$$
3		iunxun	$$⊢\bigcup _{x\in A\cup \left\{X,Y\right\}}B=\bigcup _{x\in A}B\cup \bigcup _{x\in \left\{X,Y\right\}}B$$
4	1 2	iunxprg	$$⊢\left(X\in V\wedge Y\in W\right)\to \bigcup _{x\in \left\{X,Y\right\}}B=C\cup D$$
5	4	uneq2d	$$⊢\left(X\in V\wedge Y\in W\right)\to \bigcup _{x\in A}B\cup \bigcup _{x\in \left\{X,Y\right\}}B=\bigcup _{x\in A}B\cup \left(C\cup D\right)$$
6	3 5	eqtrid	$$⊢\left(X\in V\wedge Y\in W\right)\to \bigcup _{x\in A\cup \left\{X,Y\right\}}B=\bigcup _{x\in A}B\cup \left(C\cup D\right)$$