Theorem iuneq12i

Description: Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	iuneq12i.1	$$⊢A=B$$
	iuneq12i.2	$$⊢C=D$$
Assertion	iuneq12i	$$⊢\bigcup _{x\in A}C=\bigcup _{x\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		iuneq12i.1	$$⊢A=B$$
2		iuneq12i.2	$$⊢C=D$$
3	2	eleq2i	$$⊢t\in C\leftrightarrow t\in D$$
4	1 3	rexeqbii	$$⊢\exists x\in At\in C\leftrightarrow \exists x\in Bt\in D$$
5	4	abbii	$$⊢\left\{t|\exists x\in At\in C\right\}=\left\{t|\exists x\in Bt\in D\right\}$$
6		df-iun	$$⊢\bigcup _{x\in A}C=\left\{t|\exists x\in At\in C\right\}$$
7		df-iun	$$⊢\bigcup _{x\in B}D=\left\{t|\exists x\in Bt\in D\right\}$$
8	5 6 7	3eqtr4i	$$⊢\bigcup _{x\in A}C=\bigcup _{x\in B}D$$