Theorem dfcoll2

Description: Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Assertion	dfcoll2	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		df-coll	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } )
2		imasng	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 “ { 𝑥 } ) = { 𝑦 ∣ 𝑥 𝐹 𝑦 } )
3	2	scotteqd	⊢ ( 𝑥 ∈ 𝐴 → Scott ( 𝐹 “ { 𝑥 } ) = Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } )
4	3	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } ) = ∪ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 }
5	1 4	eqtri	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 }