Theorem iuneq2f

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

	Ref	Expression
Hypotheses	iuneq2f.1	⊢ Ⅎ 𝑥 𝐴
	iuneq2f.2	⊢ Ⅎ 𝑥 𝐵
Assertion	iuneq2f	⊢ ( 𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		iuneq2f.1	⊢ Ⅎ 𝑥 𝐴
2		iuneq2f.2	⊢ Ⅎ 𝑥 𝐵
3	1 2	nfeq	⊢ Ⅎ 𝑥 𝐴 = 𝐵
4		id	⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
5		eqidd	⊢ ( 𝐴 = 𝐵 → 𝐶 = 𝐶 )
6	3 1 2 4 5	iuneq12df	⊢ ( 𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 )