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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feqmptdf.1 | |
|
2 | feqmptdf.2 | |
|
3 | feqmptdf.3 | |
|
4 | ffn | |
|
5 | fnrel | |
|
6 | nfcv | |
|
7 | 2 6 | dfrel4 | |
8 | 5 7 | sylib | |
9 | 2 1 | nffn | |
10 | nfv | |
|
11 | fnbr | |
|
12 | 11 | ex | |
13 | 12 | pm4.71rd | |
14 | eqcom | |
|
15 | fnbrfvb | |
|
16 | 14 15 | bitrid | |
17 | 16 | pm5.32da | |
18 | 13 17 | bitr4d | |
19 | 9 10 18 | opabbid | |
20 | 8 19 | eqtrd | |
21 | df-mpt | |
|
22 | 20 21 | eqtr4di | |
23 | 3 4 22 | 3syl | |