# Metamath Proof Explorer

## Theorem funbrfv

Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion funbrfv ${⊢}\mathrm{Fun}{F}\to \left({A}{F}{B}\to {F}\left({A}\right)={B}\right)$

### Proof

Step Hyp Ref Expression
1 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
2 brrelex2 ${⊢}\left(\mathrm{Rel}{F}\wedge {A}{F}{B}\right)\to {B}\in \mathrm{V}$
3 1 2 sylan ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to {B}\in \mathrm{V}$
4 breq2 ${⊢}{y}={B}\to \left({A}{F}{y}↔{A}{F}{B}\right)$
5 4 anbi2d ${⊢}{y}={B}\to \left(\left(\mathrm{Fun}{F}\wedge {A}{F}{y}\right)↔\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\right)$
6 eqeq2 ${⊢}{y}={B}\to \left({F}\left({A}\right)={y}↔{F}\left({A}\right)={B}\right)$
7 5 6 imbi12d ${⊢}{y}={B}\to \left(\left(\left(\mathrm{Fun}{F}\wedge {A}{F}{y}\right)\to {F}\left({A}\right)={y}\right)↔\left(\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to {F}\left({A}\right)={B}\right)\right)$
8 funeu ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{y}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
9 tz6.12-1 ${⊢}\left({A}{F}{y}\wedge \exists !{y}\phantom{\rule{.4em}{0ex}}{A}{F}{y}\right)\to {F}\left({A}\right)={y}$
10 8 9 sylan2 ${⊢}\left({A}{F}{y}\wedge \left(\mathrm{Fun}{F}\wedge {A}{F}{y}\right)\right)\to {F}\left({A}\right)={y}$
11 10 anabss7 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{y}\right)\to {F}\left({A}\right)={y}$
12 7 11 vtoclg ${⊢}{B}\in \mathrm{V}\to \left(\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to {F}\left({A}\right)={B}\right)$
13 3 12 mpcom ${⊢}\left(\mathrm{Fun}{F}\wedge {A}{F}{B}\right)\to {F}\left({A}\right)={B}$
14 13 ex ${⊢}\mathrm{Fun}{F}\to \left({A}{F}{B}\to {F}\left({A}\right)={B}\right)$