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