# Metamath Proof Explorer

## Theorem dffn5

Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dffn5 ${⊢}{F}Fn{A}↔{F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fnrel ${⊢}{F}Fn{A}\to \mathrm{Rel}{F}$
2 dfrel4v ${⊢}\mathrm{Rel}{F}↔{F}=\left\{⟨{x},{y}⟩|{x}{F}{y}\right\}$
3 1 2 sylib ${⊢}{F}Fn{A}\to {F}=\left\{⟨{x},{y}⟩|{x}{F}{y}\right\}$
4 fnbr ${⊢}\left({F}Fn{A}\wedge {x}{F}{y}\right)\to {x}\in {A}$
5 4 ex ${⊢}{F}Fn{A}\to \left({x}{F}{y}\to {x}\in {A}\right)$
6 5 pm4.71rd ${⊢}{F}Fn{A}\to \left({x}{F}{y}↔\left({x}\in {A}\wedge {x}{F}{y}\right)\right)$
7 eqcom ${⊢}{y}={F}\left({x}\right)↔{F}\left({x}\right)={y}$
8 fnbrfvb ${⊢}\left({F}Fn{A}\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={y}↔{x}{F}{y}\right)$
9 7 8 syl5bb ${⊢}\left({F}Fn{A}\wedge {x}\in {A}\right)\to \left({y}={F}\left({x}\right)↔{x}{F}{y}\right)$
10 9 pm5.32da ${⊢}{F}Fn{A}\to \left(\left({x}\in {A}\wedge {y}={F}\left({x}\right)\right)↔\left({x}\in {A}\wedge {x}{F}{y}\right)\right)$
11 6 10 bitr4d ${⊢}{F}Fn{A}\to \left({x}{F}{y}↔\left({x}\in {A}\wedge {y}={F}\left({x}\right)\right)\right)$
12 11 opabbidv ${⊢}{F}Fn{A}\to \left\{⟨{x},{y}⟩|{x}{F}{y}\right\}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}={F}\left({x}\right)\right)\right\}$
13 3 12 eqtrd ${⊢}{F}Fn{A}\to {F}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}={F}\left({x}\right)\right)\right\}$
14 df-mpt ${⊢}\left({x}\in {A}⟼{F}\left({x}\right)\right)=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}={F}\left({x}\right)\right)\right\}$
15 13 14 eqtr4di ${⊢}{F}Fn{A}\to {F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
16 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
17 eqid ${⊢}\left({x}\in {A}⟼{F}\left({x}\right)\right)=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
18 16 17 fnmpti ${⊢}\left({x}\in {A}⟼{F}\left({x}\right)\right)Fn{A}$
19 fneq1 ${⊢}{F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)\to \left({F}Fn{A}↔\left({x}\in {A}⟼{F}\left({x}\right)\right)Fn{A}\right)$
20 18 19 mpbiri ${⊢}{F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)\to {F}Fn{A}$
21 15 20 impbii ${⊢}{F}Fn{A}↔{F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$