Theorem mpompts

Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015)

	Ref	Expression
Assertion	mpompts	$$⊢\left(x\in A,y\in B⟼C\right)=\left(z\in \left(A\times B\right)⟼⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpomptsx	$$⊢\left(x\in A,y\in B⟼C\right)=\left(z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⟼⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\right)$$
2		iunxpconst	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=A\times B$$
3	2	mpteq1i	$$⊢\left(z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⟼⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\right)=\left(z\in \left(A\times B\right)⟼⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\right)$$
4	1 3	eqtri	$$⊢\left(x\in A,y\in B⟼C\right)=\left(z\in \left(A\times B\right)⟼⦋1^{st}\left(z\right)/x⦌⦋2^{nd}\left(z\right)/y⦌C\right)$$