Theorem dffn5f

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

	Ref	Expression
Hypothesis	dffn5f.1	⊢ Ⅎ 𝑥 𝐹
Assertion	dffn5f	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffn5f.1	⊢ Ⅎ 𝑥 𝐹
2		dffn5	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
3		nfcv	⊢ Ⅎ 𝑥 𝑧
4	1 3	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
5		nfcv	⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 )
6		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
7	4 5 6	cbvmpt	⊢ ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) )
8	7	eqeq2i	⊢ ( 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
9	2 8	bitri	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )