Theorem dfafn5a

Description: Representation of a function in terms of its values, analogous to dffn5 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	dfafn5a	|- ( 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		fnbrafvb	|- ( ( F Fn A /\ x e. A ) -> ( ( F ''' x ) = y <-> x F y ) )
9	7 8	bitrid	|- ( ( 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 ) ) )