Metamath Proof Explorer


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𝑧 ) / 𝑦 𝐶 )