Description: Express a two-argument function as a one-argument function, or vice-versa. In this version B ( x ) is not assumed to be constant w.r.t x . (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Thierry Arnoux, 31-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mpomptxf.0 | |
|
mpomptxf.1 | |
||
mpomptxf.2 | |
||
Assertion | mpomptxf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpomptxf.0 | |
|
2 | mpomptxf.1 | |
|
3 | mpomptxf.2 | |
|
4 | df-mpt | |
|
5 | df-mpo | |
|
6 | eliunxp | |
|
7 | 6 | anbi1i | |
8 | 2 | nfeq2 | |
9 | 8 | 19.41 | |
10 | 9 | exbii | |
11 | 1 | nfeq2 | |
12 | 11 | 19.41 | |
13 | 10 12 | bitri | |
14 | anass | |
|
15 | 3 | eqeq2d | |
16 | 15 | anbi2d | |
17 | 16 | pm5.32i | |
18 | 14 17 | bitri | |
19 | 18 | 2exbii | |
20 | 7 13 19 | 3bitr2i | |
21 | 20 | opabbii | |
22 | dfoprab2 | |
|
23 | 21 22 | eqtr4i | |
24 | 5 23 | eqtr4i | |
25 | 4 24 | eqtr4i | |