Metamath Proof Explorer

Theorem funeu

Description: There is exactly one value of a function. (Contributed by NM, 22-Apr-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion funeu ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$

Proof

Step Hyp Ref Expression
1 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
2 releldm ${⊢}\left(\mathrm{Rel}{F}\wedge {A}{F}{B}\right)\to {A}\in \mathrm{dom}{F}$
3 1 2 sylan ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to {A}\in \mathrm{dom}{F}$
4 eldmg ${⊢}{A}\in \mathrm{dom}{F}\to \left({A}\in \mathrm{dom}{F}↔\exists {y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
5 4 ibi ${⊢}{A}\in \mathrm{dom}{F}\to \exists {y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
6 3 5 syl ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
7 funmo ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
8 7 adantr ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
9 moeu ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
10 8 9 sylib ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\to \exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)$
11 6 10 mpd ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$