Theorem unieqd

Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995)

	Ref	Expression
Hypothesis	unieqd.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	unieqd	⊢ ( 𝜑 → ∪ 𝐴 = ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		unieqd.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		unieq	⊢ ( 𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵 )
3	1 2	syl	⊢ ( 𝜑 → ∪ 𝐴 = ∪ 𝐵 )