# Metamath Proof Explorer

## Theorem funoprabg

Description: "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007)

Ref Expression
Assertion funoprabg ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{\phi }\to \mathrm{Fun}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 mosubopt ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{\phi }\to {\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {\phi }\right)$
2 1 alrimiv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {w}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {\phi }\right)$
3 dfoprab2 ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}=\left\{⟨{w},{z}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {\phi }\right)\right\}$
4 3 funeqi ${⊢}\mathrm{Fun}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}↔\mathrm{Fun}\left\{⟨{w},{z}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {\phi }\right)\right\}$
5 funopab ${⊢}\mathrm{Fun}\left\{⟨{w},{z}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {\phi }\right)\right\}↔\forall {w}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {\phi }\right)$
6 4 5 bitr2i ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {\phi }\right)↔\mathrm{Fun}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}$
7 2 6 sylib ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{\phi }\to \mathrm{Fun}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}$