Theorem fveu

Description: The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017)

	Ref	Expression
Assertion	fveu	$$⊢\exists !xAFx\to F\left(A\right)=\bigcup \left\{x|AFx\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-fv	$$⊢F\left(A\right)=\left(\iota x|AFx\right)$$
2		iotauni	$$⊢\exists !xAFx\to \left(\iota x|AFx\right)=\bigcup \left\{x|AFx\right\}$$
3	1 2	syl5eq	$$⊢\exists !xAFx\to F\left(A\right)=\bigcup \left\{x|AFx\right\}$$