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	$$⊢A=B\to \bigcup A=\bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢A=B\to A\subseteq B$$
2	1	unissd	$$⊢A=B\to \bigcup A\subseteq \bigcup B$$
3		eqimss2	$$⊢A=B\to B\subseteq A$$
4	3	unissd	$$⊢A=B\to \bigcup B\subseteq \bigcup A$$
5	2 4	eqssd	$$⊢A=B\to \bigcup A=\bigcup B$$