Theorem funfv

Description: A simplified expression for the value of a function when we know it is a function. (Contributed by NM, 22-May-1998)

	Ref	Expression
Assertion	funfv	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup F\left[\left\{A\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
2	1	unisn	$$⊢\bigcup \left\{F\left(A\right)\right\}=F\left(A\right)$$
3		eqid	$$⊢\mathrm{dom}F=\mathrm{dom}F$$
4		df-fn	$$⊢FFn\mathrm{dom}F\leftrightarrow \left(\mathrm{Fun}F\wedge \mathrm{dom}F=\mathrm{dom}F\right)$$
5	3 4	mpbiran2	$$⊢FFn\mathrm{dom}F\leftrightarrow \mathrm{Fun}F$$
6		fnsnfv	$$⊢\left(FFn\mathrm{dom}F\wedge A\in \mathrm{dom}F\right)\to \left\{F\left(A\right)\right\}=F\left[\left\{A\right\}\right]$$
7	5 6	sylanbr	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left\{F\left(A\right)\right\}=F\left[\left\{A\right\}\right]$$
8	7	unieqd	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \bigcup \left\{F\left(A\right)\right\}=\bigcup F\left[\left\{A\right\}\right]$$
9	2 8	syl5eqr	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to F\left(A\right)=\bigcup F\left[\left\{A\right\}\right]$$
10	9	ex	$$⊢\mathrm{Fun}F\to \left(A\in \mathrm{dom}F\to F\left(A\right)=\bigcup F\left[\left\{A\right\}\right]\right)$$
11		ndmfv	$$⊢\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing$$
12		ndmima	$$⊢\neg A\in \mathrm{dom}F\to F\left[\left\{A\right\}\right]=\varnothing$$
13	12	unieqd	$$⊢\neg A\in \mathrm{dom}F\to \bigcup F\left[\left\{A\right\}\right]=\bigcup \varnothing$$
14		uni0	$$⊢\bigcup \varnothing =\varnothing$$
15	13 14	syl6eq	$$⊢\neg A\in \mathrm{dom}F\to \bigcup F\left[\left\{A\right\}\right]=\varnothing$$
16	11 15	eqtr4d	$$⊢\neg A\in \mathrm{dom}F\to F\left(A\right)=\bigcup F\left[\left\{A\right\}\right]$$
17	10 16	pm2.61d1	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup F\left[\left\{A\right\}\right]$$