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	$$⊢\phi \to A\in V$$
Assertion	collexd	$$⊢\phi \to \left(FCollA\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		collexd.1	$$⊢\phi \to A\in V$$
2		df-coll	$$⊢\left(FCollA\right)=\bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]$$
3		scottex	$$⊢ScottF\left[\left\{x\right\}\right]\in \mathrm{V}$$
4	3	a1i	$$⊢\phi \to ScottF\left[\left\{x\right\}\right]\in \mathrm{V}$$
5	4	ralrimivw	$$⊢\phi \to \forall x\in AScottF\left[\left\{x\right\}\right]\in \mathrm{V}$$
6		iunexg	$$⊢\left(A\in V\wedge \forall x\in AScottF\left[\left\{x\right\}\right]\in \mathrm{V}\right)\to \bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]\in \mathrm{V}$$
7	1 5 6	syl2anc	$$⊢\phi \to \bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]\in \mathrm{V}$$
8	2 7	eqeltrid	$$⊢\phi \to \left(FCollA\right)\in \mathrm{V}$$