Theorem dfafn5b

Description: Representation of a function in terms of its values, analogous to dffn5 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	dfafn5b	|- ( A. x e. A ( F ''' x ) e. V -> ( F Fn A <-> F = ( x e. A |-> ( F ''' x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfafn5a	|- ( F Fn A -> F = ( x e. A |-> ( F ''' x ) ) )
2		eqid	|- ( x e. A |-> ( F ''' x ) ) = ( x e. A |-> ( F ''' x ) )
3	2	fnmpt	|- ( A. x e. A ( F ''' x ) e. V -> ( x e. A |-> ( F ''' x ) ) Fn A )
4		fneq1	|- ( F = ( x e. A |-> ( F ''' x ) ) -> ( F Fn A <-> ( x e. A |-> ( F ''' x ) ) Fn A ) )
5	3 4	syl5ibrcom	|- ( A. x e. A ( F ''' x ) e. V -> ( F = ( x e. A |-> ( F ''' x ) ) -> F Fn A ) )
6	1 5	impbid2	|- ( A. x e. A ( F ''' x ) e. V -> ( F Fn A <-> F = ( x e. A |-> ( F ''' x ) ) ) )