# Metamath Proof Explorer

## Theorem dffun9

Description: Alternate definition of a function. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

Ref Expression
Assertion dffun9 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\in \mathrm{ran}{A}{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 vex ${⊢}{x}\in \mathrm{V}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 2 3 brelrn ${⊢}{x}{A}{y}\to {y}\in \mathrm{ran}{A}$
5 4 pm4.71ri ${⊢}{x}{A}{y}↔\left({y}\in \mathrm{ran}{A}\wedge {x}{A}{y}\right)$
6 5 mobii ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{ran}{A}\wedge {x}{A}{y}\right)$
7 df-rmo ${⊢}{\exists }^{*}{y}\in \mathrm{ran}{A}{x}{A}{y}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in \mathrm{ran}{A}\wedge {x}{A}{y}\right)$
8 6 7 bitr4i ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{\exists }^{*}{y}\in \mathrm{ran}{A}{x}{A}{y}$
9 8 ralbii ${⊢}\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}\in \mathrm{ran}{A}{x}{A}{y}$
10 9 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}\in \mathrm{ran}{A}{x}{A}{y}\right)$
11 1 10 bitri ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\in \mathrm{dom}{A}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\in \mathrm{ran}{A}{x}{A}{y}\right)$