Metamath Proof Explorer


Theorem nfcoll

Description: Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Hypotheses nfcoll.1
|- F/_ x F
nfcoll.2
|- F/_ x A
Assertion nfcoll
|- F/_ x ( F Coll A )

Proof

Step Hyp Ref Expression
1 nfcoll.1
 |-  F/_ x F
2 nfcoll.2
 |-  F/_ x A
3 df-coll
 |-  ( F Coll A ) = U_ y e. A Scott ( F " { y } )
4 nfcv
 |-  F/_ x { y }
5 1 4 nfima
 |-  F/_ x ( F " { y } )
6 5 nfscott
 |-  F/_ x Scott ( F " { y } )
7 2 6 nfiun
 |-  F/_ x U_ y e. A Scott ( F " { y } )
8 3 7 nfcxfr
 |-  F/_ x ( F Coll A )