Theorem fvex

Description: The value of a class exists. Corollary 6.13 of TakeutiZaring p. 27. (Contributed by NM, 30-Dec-1996)

	Ref	Expression
Assertion	fvex	$$⊢F\left(A\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-fv	$$⊢F\left(A\right)=\left(\iota x|AFx\right)$$
2		iotaex	$$⊢\left(\iota x|AFx\right)\in \mathrm{V}$$
3	1 2	eqeltri	$$⊢F\left(A\right)\in \mathrm{V}$$