# Metamath Proof Explorer

## Theorem dffun2

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

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

### Proof

Step Hyp Ref Expression
1 df-fun ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge {A}\circ {{A}}^{-1}\subseteq \mathrm{I}\right)$
2 df-id ${⊢}\mathrm{I}=\left\{⟨{y},{z}⟩|{y}={z}\right\}$
3 2 sseq2i ${⊢}{A}\circ {{A}}^{-1}\subseteq \mathrm{I}↔{A}\circ {{A}}^{-1}\subseteq \left\{⟨{y},{z}⟩|{y}={z}\right\}$
4 df-co ${⊢}{A}\circ {{A}}^{-1}=\left\{⟨{y},{z}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\right\}$
5 4 sseq1i ${⊢}{A}\circ {{A}}^{-1}\subseteq \left\{⟨{y},{z}⟩|{y}={z}\right\}↔\left\{⟨{y},{z}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\right\}\subseteq \left\{⟨{y},{z}⟩|{y}={z}\right\}$
6 ssopab2bw ${⊢}\left\{⟨{y},{z}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\right\}\subseteq \left\{⟨{y},{z}⟩|{y}={z}\right\}↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
7 3 5 6 3bitri ${⊢}{A}\circ {{A}}^{-1}\subseteq \mathrm{I}↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
8 vex ${⊢}{y}\in \mathrm{V}$
9 vex ${⊢}{x}\in \mathrm{V}$
10 8 9 brcnv ${⊢}{y}{{A}}^{-1}{x}↔{x}{A}{y}$
11 10 anbi1i ${⊢}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)↔\left({x}{A}{y}\wedge {x}{A}{z}\right)$
12 11 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\wedge {x}{A}{z}\right)$
13 12 imbi1i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
14 19.23v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
15 13 14 bitr4i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
16 15 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
17 alcom ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\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 {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
18 16 17 bitri ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
19 18 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{{A}}^{-1}{x}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
20 alcom ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\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}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
21 7 19 20 3bitri ${⊢}{A}\circ {{A}}^{-1}\subseteq \mathrm{I}↔\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)$
22 21 anbi2i ${⊢}\left(\mathrm{Rel}{A}\wedge {A}\circ {{A}}^{-1}\subseteq \mathrm{I}\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}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)\right)$
23 1 22 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}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)\right)$