This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unieq

Description: Equality theorem for class union. Exercise 15 of TakeutiZaring p. 18. (Contributed by NM, 10-Aug-1993) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by BJ, 13-Apr-2024)

		Ref	Expression
	Assertion	unieq	⊢ ( 𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqimss	⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )
2	1	unissd	⊢ ( 𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵 )
3		eqimss2	⊢ ( 𝐴 = 𝐵 → 𝐵 ⊆ 𝐴 )
4	3	unissd	⊢ ( 𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴 )
5	2 4	eqssd	⊢ ( 𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵 )