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 _xA
feqmptdf.2 _xF
feqmptdf.3 φF:AB
Assertion feqmptdf φF=xAFx

Proof

Step Hyp Ref Expression
1 feqmptdf.1 _xA
2 feqmptdf.2 _xF
3 feqmptdf.3 φF:AB
4 ffn F:ABFFnA
5 fnrel FFnARelF
6 nfcv _yF
7 2 6 dfrel4 RelFF=xy|xFy
8 5 7 sylib FFnAF=xy|xFy
9 2 1 nffn xFFnA
10 nfv yFFnA
11 fnbr FFnAxFyxA
12 11 ex FFnAxFyxA
13 12 pm4.71rd FFnAxFyxAxFy
14 eqcom y=FxFx=y
15 fnbrfvb FFnAxAFx=yxFy
16 14 15 bitrid FFnAxAy=FxxFy
17 16 pm5.32da FFnAxAy=FxxAxFy
18 13 17 bitr4d FFnAxFyxAy=Fx
19 9 10 18 opabbid FFnAxy|xFy=xy|xAy=Fx
20 8 19 eqtrd FFnAF=xy|xAy=Fx
21 df-mpt xAFx=xy|xAy=Fx
22 20 21 eqtr4di FFnAF=xAFx
23 3 4 22 3syl φF=xAFx