Definition df-coll

Description: Define the collection operation. This is similar to the image set operation " , but it uses Scott's trick to ensure the output is always a set. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Assertion	df-coll	|- ( F Coll A ) = U_ x e. A Scott ( F " { x } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1		cA	|- A
2	1 0	ccoll	|- ( F Coll A )
3		vx	|- x
4	3	cv	|- x
5	4	csn	|- { x }
6	0 5	cima	|- ( F " { x } )
7	6	cscott	|- Scott ( F " { x } )
8	3 1 7	ciun	|- U_ x e. A Scott ( F " { x } )
9	2 8	wceq	|- ( F Coll A ) = U_ x e. A Scott ( F " { x } )