![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpt2mpt | 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 |
---|---|
mpt2mpt.1 | ⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
mpt2mpt | ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunxpconst 5421 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
2 | 1 | mpteq1i 4974 | . 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) |
3 | mpt2mpt.1 | . . 3 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) | |
4 | 3 | mpt2mptx 7028 | . 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
5 | 2, 4 | eqtr3i 2804 | 1 ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 {csn 4398 〈cop 4404 ∪ ciun 4753 ↦ cmpt 4965 × cxp 5353 ↦ cmpt2 6924 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-iun 4755 df-opab 4949 df-mpt 4966 df-xp 5361 df-rel 5362 df-oprab 6926 df-mpt2 6927 |
This theorem is referenced by: fconstmpt2 7032 fnov 7045 fmpt2co 7541 xpf1o 8410 resfval2 16938 catcisolem 17141 xpccatid 17214 curf2ndf 17273 evlslem4 19904 mdetunilem9 20831 txbas 21779 cnmpt1st 21880 cnmpt2nd 21881 cnmpt2c 21882 cnmpt2t 21885 txhmeo 22015 txswaphmeolem 22016 ptuncnv 22019 ptunhmeo 22020 xpstopnlem1 22021 xkohmeo 22027 prdstmdd 22335 ucnimalem 22492 fmucndlem 22503 fsum2cn 23082 fimaproj 30498 curfv 34014 idfusubc0 42880 lmod1zr 43297 |
Copyright terms: Public domain | W3C validator |