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 | ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 ) | |
| Assertion | mpompt | ⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpompt.1 | ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 ) | |
| 2 | iunxpconst | ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ( 𝐴 × 𝐵 ) | |
| 3 | 2 | mpteq1i | ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ 𝐶 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 ) |
| 4 | 1 | mpomptx | ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) |
| 5 | 3 4 | eqtr3i | ⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) |