Definition df-coll 44270

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 44269	. 2 class (𝐹 Coll 𝐴)
4		vx	. . 3 setvar 𝑥
5	4	cv 1539	. . . . . 6 class 𝑥
6	5	csn 4626	. . . . 5 class {𝑥}
7	2, 6	cima 5688	. . . 4 class (𝐹 “ {𝑥})
8	7	cscott 44254	. . 3 class Scott (𝐹 “ {𝑥})
9	4, 1, 8	ciun 4991	. 2 class ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})
10	3, 9	wceq 1540	1 wff (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})

This definition is referenced by:  dfcoll2  44271  colleq12d  44272  nfcoll  44275  collexd  44276