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	|- F/_ x A
	feqmptdf.2	|- F/_ x F
	feqmptdf.3	|- ( ph -> F : A --> B )
Assertion	feqmptdf	|- ( ph -> F = ( x e. A |-> ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		feqmptdf.1	|- F/_ x A
2		feqmptdf.2	|- F/_ x F
3		feqmptdf.3	|- ( ph -> F : A --> B )
4		ffn	|- ( F : A --> B -> F Fn A )
5		fnrel	|- ( F Fn A -> Rel F )
6		nfcv	|- F/_ y F
7	2 6	dfrel4	|- ( Rel F <-> F = { <. x , y >. | x F y } )
8	5 7	sylib	|- ( F Fn A -> F = { <. x , y >. | x F y } )
9	2 1	nffn	|- F/ x F Fn A
10		nfv	|- F/ y F Fn A
11		fnbr	|- ( ( F Fn A /\ x F y ) -> x e. A )
12	11	ex	|- ( F Fn A -> ( x F y -> x e. A ) )
13	12	pm4.71rd	|- ( F Fn A -> ( x F y <-> ( x e. A /\ x F y ) ) )
14		eqcom	|- ( y = ( F ` x ) <-> ( F ` x ) = y )
15		fnbrfvb	|- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
16	14 15	bitrid	|- ( ( F Fn A /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
17	16	pm5.32da	|- ( F Fn A -> ( ( x e. A /\ y = ( F ` x ) ) <-> ( x e. A /\ x F y ) ) )
18	13 17	bitr4d	|- ( F Fn A -> ( x F y <-> ( x e. A /\ y = ( F ` x ) ) ) )
19	9 10 18	opabbid	|- ( F Fn A -> { <. x , y >. | x F y } = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
20	8 19	eqtrd	|- ( F Fn A -> F = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
21		df-mpt	|- ( x e. A |-> ( F ` x ) ) = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) }
22	20 21	eqtr4di	|- ( F Fn A -> F = ( x e. A |-> ( F ` x ) ) )
23	3 4 22	3syl	|- ( ph -> F = ( x e. A |-> ( F ` x ) ) )