Theorem colleq12d

Description: Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	colleq12d.1	$$⊢\phi \to F=G$$
	colleq12d.2	$$⊢\phi \to A=B$$
Assertion	colleq12d	$$⊢\phi \to \left(FCollA\right)=\left(GCollB\right)$$

Proof

Step	Hyp	Ref	Expression
1		colleq12d.1	$$⊢\phi \to F=G$$
2		colleq12d.2	$$⊢\phi \to A=B$$
3	1	imaeq1d	$$⊢\phi \to F\left[\left\{x\right\}\right]=G\left[\left\{x\right\}\right]$$
4	3	scotteqd	$$⊢\phi \to ScottF\left[\left\{x\right\}\right]=ScottG\left[\left\{x\right\}\right]$$
5	2 4	iuneq12d	$$⊢\phi \to \bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]=\bigcup _{x\in B}ScottG\left[\left\{x\right\}\right]$$
6		df-coll	$$⊢\left(FCollA\right)=\bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]$$
7		df-coll	$$⊢\left(GCollB\right)=\bigcup _{x\in B}ScottG\left[\left\{x\right\}\right]$$
8	5 6 7	3eqtr4g	$$⊢\phi \to \left(FCollA\right)=\left(GCollB\right)$$