Theorem mpompt

Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013) (Revised by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypothesis	mpompt.1	$$⊢z=⟨x,y⟩\to C=D$$
Assertion	mpompt	$$⊢\left(z\in \left(A\times B\right)⟼C\right)=\left(x\in A,y\in B⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpompt.1	$$⊢z=⟨x,y⟩\to C=D$$
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)⟼C\right)=\left(z\in \left(A\times B\right)⟼C\right)$$
4	1	mpomptx	$$⊢\left(z\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⟼C\right)=\left(x\in A,y\in B⟼D\right)$$
5	3 4	eqtr3i	$$⊢\left(z\in \left(A\times B\right)⟼C\right)=\left(x\in A,y\in B⟼D\right)$$