Theorem iunxprg

Description: A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018)

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

Proof

Step	Hyp	Ref	Expression
1		iunxprg.1	$$⊢x=A\to C=D$$
2		iunxprg.2	$$⊢x=B\to C=E$$
3		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
4		iuneq1	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}\to \bigcup _{x\in \left\{A,B\right\}}C=\bigcup _{x\in \left\{A\right\}\cup \left\{B\right\}}C$$
5	3 4	ax-mp	$$⊢\bigcup _{x\in \left\{A,B\right\}}C=\bigcup _{x\in \left\{A\right\}\cup \left\{B\right\}}C$$
6		iunxun	$$⊢\bigcup _{x\in \left\{A\right\}\cup \left\{B\right\}}C=\bigcup _{x\in \left\{A\right\}}C\cup \bigcup _{x\in \left\{B\right\}}C$$
7	5 6	eqtri	$$⊢\bigcup _{x\in \left\{A,B\right\}}C=\bigcup _{x\in \left\{A\right\}}C\cup \bigcup _{x\in \left\{B\right\}}C$$
8	1	iunxsng	$$⊢A\in V\to \bigcup _{x\in \left\{A\right\}}C=D$$
9	8	adantr	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcup _{x\in \left\{A\right\}}C=D$$
10	2	iunxsng	$$⊢B\in W\to \bigcup _{x\in \left\{B\right\}}C=E$$
11	10	adantl	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcup _{x\in \left\{B\right\}}C=E$$
12	9 11	uneq12d	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcup _{x\in \left\{A\right\}}C\cup \bigcup _{x\in \left\{B\right\}}C=D\cup E$$
13	7 12	syl5eq	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcup _{x\in \left\{A,B\right\}}C=D\cup E$$