Theorem dfcoll2

Description: Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Assertion	dfcoll2	|- ( F Coll A ) = U_ x e. A Scott { y | x F y }

Proof

Step	Hyp	Ref	Expression
1		df-coll	|- ( F Coll A ) = U_ x e. A Scott ( F " { x } )
2		imasng	|- ( x e. A -> ( F " { x } ) = { y | x F y } )
3	2	scotteqd	|- ( x e. A -> Scott ( F " { x } ) = Scott { y | x F y } )
4	3	iuneq2i	|- U_ x e. A Scott ( F " { x } ) = U_ x e. A Scott { y | x F y }
5	1 4	eqtri	|- ( F Coll A ) = U_ x e. A Scott { y | x F y }