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 >. -> C = D )
Assertion	mpompt	|- ( z e. ( A X. B ) |-> C ) = ( x e. A , y e. B |-> D )

Proof

Step	Hyp	Ref	Expression
1		mpompt.1	|- ( z = <. x , y >. -> C = D )
2		iunxpconst	|- U_ x e. A ( { x } X. B ) = ( A X. B )
3	2	mpteq1i	|- ( z e. U_ x e. A ( { x } X. B ) |-> C ) = ( z e. ( A X. B ) |-> C )
4	1	mpomptx	|- ( z e. U_ x e. A ( { x } X. B ) |-> C ) = ( x e. A , y e. B |-> D )
5	3 4	eqtr3i	|- ( z e. ( A X. B ) |-> C ) = ( x e. A , y e. B |-> D )