Metamath Proof Explorer


Theorem mpomptxf

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 _xC
mpomptxf.1 _yC
mpomptxf.2 z=xyC=D
Assertion mpomptxf zxAx×BC=xA,yBD

Proof

Step Hyp Ref Expression
1 mpomptxf.0 _xC
2 mpomptxf.1 _yC
3 mpomptxf.2 z=xyC=D
4 df-mpt zxAx×BC=zw|zxAx×Bw=C
5 df-mpo xA,yBD=xyw|xAyBw=D
6 eliunxp zxAx×Bxyz=xyxAyB
7 6 anbi1i zxAx×Bw=Cxyz=xyxAyBw=C
8 2 nfeq2 yw=C
9 8 19.41 yz=xyxAyBw=Cyz=xyxAyBw=C
10 9 exbii xyz=xyxAyBw=Cxyz=xyxAyBw=C
11 1 nfeq2 xw=C
12 11 19.41 xyz=xyxAyBw=Cxyz=xyxAyBw=C
13 10 12 bitri xyz=xyxAyBw=Cxyz=xyxAyBw=C
14 anass z=xyxAyBw=Cz=xyxAyBw=C
15 3 eqeq2d z=xyw=Cw=D
16 15 anbi2d z=xyxAyBw=CxAyBw=D
17 16 pm5.32i z=xyxAyBw=Cz=xyxAyBw=D
18 14 17 bitri z=xyxAyBw=Cz=xyxAyBw=D
19 18 2exbii xyz=xyxAyBw=Cxyz=xyxAyBw=D
20 7 13 19 3bitr2i zxAx×Bw=Cxyz=xyxAyBw=D
21 20 opabbii zw|zxAx×Bw=C=zw|xyz=xyxAyBw=D
22 dfoprab2 xyw|xAyBw=D=zw|xyz=xyxAyBw=D
23 21 22 eqtr4i zw|zxAx×Bw=C=xyw|xAyBw=D
24 5 23 eqtr4i xA,yBD=zw|zxAx×Bw=C
25 4 24 eqtr4i zxAx×BC=xA,yBD