# 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)$
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 9, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}