Metamath Proof Explorer


Theorem dfcoll2

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

Ref Expression
Assertion dfcoll2 F Coll A = x A Scott y | x F y

Proof

Step Hyp Ref Expression
1 df-coll F Coll A = x A Scott F x
2 imasng x A F x = y | x F y
3 2 scotteqd x A Scott F x = Scott y | x F y
4 3 iuneq2i x A Scott F x = x A Scott y | x F y
5 1 4 eqtri F Coll A = x A Scott y | x F y