Theorem iuneq2f

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

	Ref	Expression
Hypotheses	iuneq2f.1	|- F/_ x A
	iuneq2f.2	|- F/_ x B
Assertion	iuneq2f	|- ( A = B -> U_ x e. A C = U_ x e. B C )

Proof

Step	Hyp	Ref	Expression
1		iuneq2f.1	|- F/_ x A
2		iuneq2f.2	|- F/_ x B
3	1 2	nfeq	|- F/ x A = B
4		id	|- ( A = B -> A = B )
5		eqidd	|- ( A = B -> C = C )
6	3 1 2 4 5	iuneq12df	|- ( A = B -> U_ x e. A C = U_ x e. B C )