Definition df-coll 44994

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.)

Assertion

Ref	Expression
df-coll	⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})

Distinct variable groups:   𝑥,𝐹   𝑥,𝐴

Detailed syntax breakdown of Definition df-coll

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cF	. . 3 class 𝐹
3	1, 2	ccoll 44993	. 2 class (𝐹 Coll 𝐴)
4		vx	. . 3 setvar 𝑥
5	4	cv 1569	. . . . . 6 class 𝑥
6	5	csn 4591	. . . . 5 class {𝑥}
7	2, 6	cima 5666	. . . 4 class (𝐹 “ {𝑥})
8	7	cscott 9860	. . 3 class Scott (𝐹 “ {𝑥})
9	4, 1, 8	ciun 4958	. 2 class ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})
10	3, 9	wceq 1570	1 wff (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})

This definition is used by:  dfcoll2  44995  colleq12d  44996  nfcoll  44999  collexd  45000