# Metamath Proof Explorer

## Theorem dffun5

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dffun5 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dffun3 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)\right)$
2 df-br ${⊢}{x}{A}{y}↔⟨{x},{y}⟩\in {A}$
3 2 imbi1i ${⊢}\left({x}{A}{y}\to {y}={z}\right)↔\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)$
4 3 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)$
5 4 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)$
6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)$
7 6 anbi2i ${⊢}\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)\right)↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)\right)$
8 1 7 bitri ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)\right)$