# Metamath Proof Explorer

## Theorem funmo

Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998)

Ref Expression
Assertion funmo ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$

### Proof

Step Hyp Ref Expression
1 dffun6 ${⊢}\mathrm{Fun}{F}↔\left(\mathrm{Rel}{F}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
2 1 simplbi ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
3 brrelex1 ${⊢}\left(\mathrm{Rel}{F}\wedge {A}{F}{y}\right)\to {A}\in \mathrm{V}$
4 3 ex ${⊢}\mathrm{Rel}{F}\to \left({A}{F}{y}\to {A}\in \mathrm{V}\right)$
5 2 4 syl ${⊢}\mathrm{Fun}{F}\to \left({A}{F}{y}\to {A}\in \mathrm{V}\right)$
6 5 ancrd ${⊢}\mathrm{Fun}{F}\to \left({A}{F}{y}\to \left({A}\in \mathrm{V}\wedge {A}{F}{y}\right)\right)$
7 6 alrimiv ${⊢}\mathrm{Fun}{F}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({A}{F}{y}\to \left({A}\in \mathrm{V}\wedge {A}{F}{y}\right)\right)$
8 breq1 ${⊢}{x}={A}\to \left({x}{F}{y}↔{A}{F}{y}\right)$
9 8 mobidv ${⊢}{x}={A}\to \left({\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
10 9 imbi2d ${⊢}{x}={A}\to \left(\left(\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)↔\left(\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)\right)$
11 1 simprbi ${⊢}\mathrm{Fun}{F}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}$
12 11 19.21bi ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}$
13 10 12 vtoclg ${⊢}{A}\in \mathrm{V}\to \left(\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
14 13 com12 ${⊢}\mathrm{Fun}{F}\to \left({A}\in \mathrm{V}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
15 moanimv ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{V}\wedge {A}{F}{y}\right)↔\left({A}\in \mathrm{V}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
16 14 15 sylibr ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{V}\wedge {A}{F}{y}\right)$
17 moim ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({A}{F}{y}\to \left({A}\in \mathrm{V}\wedge {A}{F}{y}\right)\right)\to \left({\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{V}\wedge {A}{F}{y}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
18 7 16 17 sylc ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$