![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpompt | Structured version Visualization version GIF version |
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 |
---|---|
mpompt.1 | ⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
mpompt | ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunxpconst 5760 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
2 | 1 | mpteq1i 5243 | . 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) |
3 | mpompt.1 | . . 3 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) | |
4 | 3 | mpomptx 7545 | . 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
5 | 2, 4 | eqtr3i 2764 | 1 ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 {csn 4630 〈cop 4636 ∪ ciun 4995 ↦ cmpt 5230 × cxp 5686 ∈ cmpo 7432 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-iun 4997 df-opab 5210 df-mpt 5231 df-xp 5694 df-rel 5695 df-oprab 7434 df-mpo 7435 |
This theorem is referenced by: fconstmpo 7549 fnov 7563 fmpoco 8118 fimaproj 8158 xpf1o 9177 resfval2 17943 idfusubc0 17949 catcisolem 18163 xpccatid 18243 curf2ndf 18303 evlslem4 22117 mdetunilem9 22641 txbas 23590 cnmpt1st 23691 cnmpt2nd 23692 cnmpt2c 23693 cnmpt2t 23696 txhmeo 23826 txswaphmeolem 23827 ptuncnv 23830 ptunhmeo 23831 xpstopnlem1 23832 xkohmeo 23838 prdstmdd 24147 ucnimalem 24304 fmucndlem 24315 fsum2cn 24908 elrgspnlem2 33232 curfv 37586 aks6d1c2p1 42099 aks6d1c3 42104 aks6d1c4 42105 aks6d1c6lem2 42152 aks6d1c6lem4 42154 aks6d1c7lem1 42161 fmpocos 42253 lmod1zr 48338 2arymaptf 48501 |
Copyright terms: Public domain | W3C validator |