Theorem colleq2

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

	Ref	Expression
Assertion	colleq2	$$⊢A=B\to \left(FCollA\right)=\left(FCollB\right)$$

Proof

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