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 = ( x e. A |-> ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnrel	|- ( F Fn A -> Rel F )
2		dfrel4v	|- ( Rel F <-> F = { <. x , y >. | x F y } )
3	1 2	sylib	|- ( F Fn A -> F = { <. x , y >. | x F y } )
4		fnbr	|- ( ( F Fn A /\ x F y ) -> x e. A )
5	4	ex	|- ( F Fn A -> ( x F y -> x e. A ) )
6	5	pm4.71rd	|- ( F Fn A -> ( x F y <-> ( x e. A /\ x F y ) ) )
7		eqcom	|- ( y = ( F ` x ) <-> ( F ` x ) = y )
8		fnbrfvb	|- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
9	7 8	syl5bb	|- ( ( F Fn A /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
10	9	pm5.32da	|- ( F Fn A -> ( ( x e. A /\ y = ( F ` x ) ) <-> ( x e. A /\ x F y ) ) )
11	6 10	bitr4d	|- ( F Fn A -> ( x F y <-> ( x e. A /\ y = ( F ` x ) ) ) )
12	11	opabbidv	|- ( F Fn A -> { <. x , y >. | x F y } = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
13	3 12	eqtrd	|- ( F Fn A -> F = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
14		df-mpt	|- ( x e. A |-> ( F ` x ) ) = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) }
15	13 14	eqtr4di	|- ( F Fn A -> F = ( x e. A |-> ( F ` x ) ) )
16		fvex	|- ( F ` x ) e. _V
17		eqid	|- ( x e. A |-> ( F ` x ) ) = ( x e. A |-> ( F ` x ) )
18	16 17	fnmpti	|- ( x e. A |-> ( F ` x ) ) Fn A
19		fneq1	|- ( F = ( x e. A |-> ( F ` x ) ) -> ( F Fn A <-> ( x e. A |-> ( F ` x ) ) Fn A ) )
20	18 19	mpbiri	|- ( F = ( x e. A |-> ( F ` x ) ) -> F Fn A )
21	15 20	impbii	|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )