Definition df-coll 41758

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 41757	. 2 class (𝐹 Coll 𝐴)
4		vx	. . 3 setvar 𝑥
5	4	cv 1538	. . . . . 6 class 𝑥
6	5	csn 4558	. . . . 5 class {𝑥}
7	2, 6	cima 5583	. . . 4 class (𝐹 “ {𝑥})
8	7	cscott 41742	. . 3 class Scott (𝐹 “ {𝑥})
9	4, 1, 8	ciun 4921	. 2 class ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})
10	3, 9	wceq 1539	1 wff (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})

This definition is referenced by:  dfcoll2  41759  colleq12d  41760  nfcoll  41763  collexd  41764