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	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝑉 → ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfafn5a	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) )
2		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) )
3	2	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) Fn 𝐴 )
4		fneq1	⊢ ( 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) Fn 𝐴 ) )
5	3 4	syl5ibrcom	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝑉 → ( 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) → 𝐹 Fn 𝐴 ) )
6	1 5	impbid2	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝑉 → ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) ) )