Definition df-coll 40671

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 40670	. 2 class (𝐹 Coll 𝐴)
4		vx	. . 3 setvar 𝑥
5	4	cv 1535	. . . . . 6 class 𝑥
6	5	csn 4560	. . . . 5 class {𝑥}
7	2, 6	cima 5551	. . . 4 class (𝐹 “ {𝑥})
8	7	cscott 40655	. . 3 class Scott (𝐹 “ {𝑥})
9	4, 1, 8	ciun 4912	. 2 class ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})
10	3, 9	wceq 1536	1 wff (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})

This definition is referenced by:  dfcoll2  40672  colleq12d  40673  nfcoll  40676  collexd  40677