Theorem dffn5f

Description: Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypothesis	dffn5f.1	|- F/_ x F
Assertion	dffn5f	|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffn5f.1	|- F/_ x F
2		dffn5	|- ( F Fn A <-> F = ( z e. A |-> ( F ` z ) ) )
3		nfcv	|- F/_ x z
4	1 3	nffv	|- F/_ x ( F ` z )
5		nfcv	|- F/_ z ( F ` x )
6		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
7	4 5 6	cbvmpt	|- ( z e. A |-> ( F ` z ) ) = ( x e. A |-> ( F ` x ) )
8	7	eqeq2i	|- ( F = ( z e. A |-> ( F ` z ) ) <-> F = ( x e. A |-> ( F ` x ) ) )
9	2 8	bitri	|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )