Theorem funressnvmo

Description: A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022)

	Ref	Expression
Assertion	funressnvmo	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{x\right\}}\right)\to {\exists }^{*}yxFy$$

Proof

Step	Hyp	Ref	Expression
1		dffun6	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{x\right\}}\right)\leftrightarrow \left(\mathrm{Rel}\left({F\upharpoonright }_{\left\{x\right\}}\right)\wedge \forall z{\exists }^{*}yz\left({F\upharpoonright }_{\left\{x\right\}}\right)y\right)$$
2		breq1	$$⊢x=z\to \left(x\left({F\upharpoonright }_{\left\{x\right\}}\right)y\leftrightarrow z\left({F\upharpoonright }_{\left\{x\right\}}\right)y\right)$$
3	2	equcoms	$$⊢z=x\to \left(x\left({F\upharpoonright }_{\left\{x\right\}}\right)y\leftrightarrow z\left({F\upharpoonright }_{\left\{x\right\}}\right)y\right)$$
4	3	biimpd	$$⊢z=x\to \left(x\left({F\upharpoonright }_{\left\{x\right\}}\right)y\to z\left({F\upharpoonright }_{\left\{x\right\}}\right)y\right)$$
5	4	moimdv	$$⊢z=x\to \left({\exists }^{*}yz\left({F\upharpoonright }_{\left\{x\right\}}\right)y\to {\exists }^{*}yx\left({F\upharpoonright }_{\left\{x\right\}}\right)y\right)$$
6	5	spimvw	$$⊢\forall z{\exists }^{*}yz\left({F\upharpoonright }_{\left\{x\right\}}\right)y\to {\exists }^{*}yx\left({F\upharpoonright }_{\left\{x\right\}}\right)y$$
7		vsnid	$$⊢x\in \left\{x\right\}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	8	brresi	$$⊢x\left({F\upharpoonright }_{\left\{x\right\}}\right)y\leftrightarrow \left(x\in \left\{x\right\}\wedge xFy\right)$$
10	7 9	mpbiran	$$⊢x\left({F\upharpoonright }_{\left\{x\right\}}\right)y\leftrightarrow xFy$$
11	10	biimpri	$$⊢xFy\to x\left({F\upharpoonright }_{\left\{x\right\}}\right)y$$
12	11	moimi	$$⊢{\exists }^{*}yx\left({F\upharpoonright }_{\left\{x\right\}}\right)y\to {\exists }^{*}yxFy$$
13	6 12	syl	$$⊢\forall z{\exists }^{*}yz\left({F\upharpoonright }_{\left\{x\right\}}\right)y\to {\exists }^{*}yxFy$$
14	1 13	simplbiim	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{x\right\}}\right)\to {\exists }^{*}yxFy$$