Metamath Proof Explorer


Theorem collexd

Description: The output of the collection operation is a set if the second input is. (Contributed by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Hypothesis collexd.1 φ A V
Assertion collexd φ F Coll A V

Proof

Step Hyp Ref Expression
1 collexd.1 φ A V
2 df-coll F Coll A = x A Scott F x
3 scottex2 Scott F x V
4 3 a1i φ Scott F x V
5 4 ralrimivw φ x A Scott F x V
6 iunexg A V x A Scott F x V x A Scott F x V
7 1 5 6 syl2anc φ x A Scott F x V
8 2 7 eqeltrid φ F Coll A V