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 𝑥 𝐹
nfcoll.2 𝑥 𝐴
Assertion nfcoll 𝑥 ( 𝐹 Coll 𝐴 )

Proof

Step Hyp Ref Expression
1 nfcoll.1 𝑥 𝐹
2 nfcoll.2 𝑥 𝐴
3 df-coll ( 𝐹 Coll 𝐴 ) = 𝑦𝐴 Scott ( 𝐹 “ { 𝑦 } )
4 nfcv 𝑥 { 𝑦 }
5 1 4 nfima 𝑥 ( 𝐹 “ { 𝑦 } )
6 5 nfscott 𝑥 Scott ( 𝐹 “ { 𝑦 } )
7 2 6 nfiun 𝑥 𝑦𝐴 Scott ( 𝐹 “ { 𝑦 } )
8 3 7 nfcxfr 𝑥 ( 𝐹 Coll 𝐴 )