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	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mpomptsx	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
2		iunxpconst	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ( 𝐴 × 𝐵 )
3	2	mpteq1i	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
4	1 3	eqtri	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )