Theorem colleq12d

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

	Ref	Expression
Hypotheses	colleq12d.1	|- ( ph -> F = G )
	colleq12d.2	|- ( ph -> A = B )
Assertion	colleq12d	|- ( ph -> ( F Coll A ) = ( G Coll B ) )

Proof

Step	Hyp	Ref	Expression
1		colleq12d.1	|- ( ph -> F = G )
2		colleq12d.2	|- ( ph -> A = B )
3	1	imaeq1d	|- ( ph -> ( F " { x } ) = ( G " { x } ) )
4	3	scotteqd	|- ( ph -> Scott ( F " { x } ) = Scott ( G " { x } ) )
5	2 4	iuneq12d	|- ( ph -> U_ x e. A Scott ( F " { x } ) = U_ x e. B Scott ( G " { x } ) )
6		df-coll	|- ( F Coll A ) = U_ x e. A Scott ( F " { x } )
7		df-coll	|- ( G Coll B ) = U_ x e. B Scott ( G " { x } )
8	5 6 7	3eqtr4g	|- ( ph -> ( F Coll A ) = ( G Coll B ) )