This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )