# Metamath Proof Explorer

## Theorem dffun3

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

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 dffun2 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)\right)$
2 breq2 ${⊢}{y}={z}\to \left({x}{A}{y}↔{x}{A}{z}\right)$
3 2 mo4 ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
4 df-mo ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)$
5 3 4 bitr3i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)$
6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\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)$
7 6 anbi2i ${⊢}\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\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}{A}{y}\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}{A}{y}\to {y}={z}\right)\right)$