# Metamath Proof Explorer

## Theorem dffun8

Description: Alternate definition of a function. One possibility for the definition of a function in Enderton p. 42. Compare dffun7 . (Contributed by NM, 4-Nov-2002) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion dffun8 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$

### Proof

Step Hyp Ref Expression
1 dffun7 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$
2 moeu ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\to \exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$
3 vex ${⊢}{x}\in \mathrm{V}$
4 3 eldm ${⊢}{x}\in \mathrm{dom}{A}↔\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
5 pm5.5 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\to \left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\to \exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$
6 4 5 sylbi ${⊢}{x}\in \mathrm{dom}{A}\to \left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\to \exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$
7 2 6 syl5bb ${⊢}{x}\in \mathrm{dom}{A}\to \left({\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$
8 7 ralbiia ${⊢}\forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
9 8 anbi2i ${⊢}\left(\mathrm{Rel}{A}\wedge \forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)↔\left(\mathrm{Rel}{A}\wedge \forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$
10 1 9 bitri ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right)$