# Metamath Proof Explorer

## Theorem dffun4

Description: Alternate definition of a function. Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dffun4 ${⊢}\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},{y}⟩\in {A}\wedge ⟨{x},{z}⟩\in {A}\right)\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 df-br ${⊢}{x}{A}{y}↔⟨{x},{y}⟩\in {A}$
3 df-br ${⊢}{x}{A}{z}↔⟨{x},{z}⟩\in {A}$
4 2 3 anbi12i ${⊢}\left({x}{A}{y}\wedge {x}{A}{z}\right)↔\left(⟨{x},{y}⟩\in {A}\wedge ⟨{x},{z}⟩\in {A}\right)$
5 4 imbi1i ${⊢}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\left(\left(⟨{x},{y}⟩\in {A}\wedge ⟨{x},{z}⟩\in {A}\right)\to {y}={z}\right)$
6 5 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {A}\wedge ⟨{x},{z}⟩\in {A}\right)\to {y}={z}\right)$
7 6 2albii ${⊢}\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}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {A}\wedge ⟨{x},{z}⟩\in {A}\right)\to {y}={z}\right)$
8 7 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}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {A}\wedge ⟨{x},{z}⟩\in {A}\right)\to {y}={z}\right)\right)$
9 1 8 bitri ${⊢}\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},{y}⟩\in {A}\wedge ⟨{x},{z}⟩\in {A}\right)\to {y}={z}\right)\right)$