Theorem funfv2

Description: The value of a function. Definition of function value in Enderton p. 43. (Contributed by NM, 22-May-1998)

	Ref	Expression
Assertion	funfv2	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup \left\{y|AFy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funfv	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup F\left[\left\{A\right\}\right]$$
2		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
3		relimasn	$$⊢\mathrm{Rel}F\to F\left[\left\{A\right\}\right]=\left\{y|AFy\right\}$$
4	2 3	syl	$$⊢\mathrm{Fun}F\to F\left[\left\{A\right\}\right]=\left\{y|AFy\right\}$$
5	4	unieqd	$$⊢\mathrm{Fun}F\to \bigcup F\left[\left\{A\right\}\right]=\bigcup \left\{y|AFy\right\}$$
6	1 5	eqtrd	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup \left\{y|AFy\right\}$$