Theorem feqmptdf

Description: Deduction form of dffn5f . (Contributed by Mario Carneiro, 8-Jan-2015) (Revised by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	feqmptdf.1	⊢ Ⅎ 𝑥 𝐴
	feqmptdf.2	⊢ Ⅎ 𝑥 𝐹
	feqmptdf.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	feqmptdf	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		feqmptdf.1	⊢ Ⅎ 𝑥 𝐴
2		feqmptdf.2	⊢ Ⅎ 𝑥 𝐹
3		feqmptdf.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
4		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
5		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
6		nfcv	⊢ Ⅎ 𝑦 𝐹
7	2 6	dfrel4	⊢ ( Rel 𝐹 ↔ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } )
8	5 7	sylib	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } )
9	2 1	nffn	⊢ Ⅎ 𝑥 𝐹 Fn 𝐴
10		nfv	⊢ Ⅎ 𝑦 𝐹 Fn 𝐴
11		fnbr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 𝐹 𝑦 ) → 𝑥 ∈ 𝐴 )
12	11	ex	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 → 𝑥 ∈ 𝐴 ) )
13	12	pm4.71rd	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) )
14		eqcom	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 )
15		fnbrfvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
16	14 15	bitrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
17	16	pm5.32da	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) )
18	13 17	bitr4d	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
19	9 10 18	opabbid	⊢ ( 𝐹 Fn 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) } )
20	8 19	eqtrd	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) } )
21		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) }
22	20 21	eqtr4di	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
23	3 4 22	3syl	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )