Theorem colleq1

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

	Ref	Expression
Assertion	colleq1	$$⊢F=G\to \left(FCollA\right)=\left(GCollA\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢F=G\to F=G$$
2		eqidd	$$⊢F=G\to A=A$$
3	1 2	colleq12d	$$⊢F=G\to \left(FCollA\right)=\left(GCollA\right)$$