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

Proof

Step	Hyp	Ref	Expression
1		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2		dfrel4v	⊢ ( Rel 𝐹 ↔ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } )
3	1 2	sylib	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } )
4		fnbr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 𝐹 𝑦 ) → 𝑥 ∈ 𝐴 )
5	4	ex	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 → 𝑥 ∈ 𝐴 ) )
6	5	pm4.71rd	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) )
7		eqcom	⊢ ( 𝑦 = ( 𝐹 ''' 𝑥 ) ↔ ( 𝐹 ''' 𝑥 ) = 𝑦 )
8		fnbrafvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ''' 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
9	7 8	bitrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ''' 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
10	9	pm5.32da	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ''' 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) )
11	6 10	bitr4d	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ''' 𝑥 ) ) ) )
12	11	opabbidv	⊢ ( 𝐹 Fn 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ''' 𝑥 ) ) } )
13	3 12	eqtrd	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ''' 𝑥 ) ) } )
14		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ''' 𝑥 ) ) }
15	13 14	eqtr4di	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) )