Theorem dffn5

Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	dffn5	⊢ ( 𝐹 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		fnbrfvb	⊢ ( ( 𝐹 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 𝐴 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
16		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
17		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) )
18	16 17	fnmpti	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) Fn 𝐴
19		fneq1	⊢ ( 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) Fn 𝐴 ) )
20	18 19	mpbiri	⊢ ( 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) → 𝐹 Fn 𝐴 )
21	15 20	impbii	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )