Theorem iuneq2f

Description: Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018)

	Ref	Expression
Hypotheses	iuneq2f.1	$$⊢\underset{\_}{Ⅎ}xA$$
	iuneq2f.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	iuneq2f	$$⊢A=B\to \bigcup _{x\in A}C=\bigcup _{x\in B}C$$

Proof

Step	Hyp	Ref	Expression
1		iuneq2f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		iuneq2f.2	$$⊢\underset{\_}{Ⅎ}xB$$
3	1 2	nfeq	$$⊢ℲxA=B$$
4		id	$$⊢A=B\to A=B$$
5		eqidd	$$⊢A=B\to C=C$$
6	3 1 2 4 5	iuneq12df	$$⊢A=B\to \bigcup _{x\in A}C=\bigcup _{x\in B}C$$