![]() |
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 5408 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
2 | mpteq1 4960 | . . 3 ⊢ (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) → (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) |
4 | mpt2mpt.1 | . . 3 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) | |
5 | 4 | mpt2mptx 7011 | . 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
6 | 3, 5 | eqtr3i 2851 | 1 ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 {csn 4397 〈cop 4403 ∪ ciun 4740 ↦ cmpt 4952 × cxp 5340 ↦ cmpt2 6907 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-iun 4742 df-opab 4936 df-mpt 4953 df-xp 5348 df-rel 5349 df-oprab 6909 df-mpt2 6910 |
This theorem is referenced by: fconstmpt2 7015 fnov 7028 fmpt2co 7524 xpf1o 8391 resfval2 16905 catcisolem 17108 xpccatid 17181 curf2ndf 17240 evlslem4 19868 mdetunilem9 20794 txbas 21741 cnmpt1st 21842 cnmpt2nd 21843 cnmpt2c 21844 cnmpt2t 21847 txhmeo 21977 txswaphmeolem 21978 ptuncnv 21981 ptunhmeo 21982 xpstopnlem1 21983 xkohmeo 21989 prdstmdd 22297 ucnimalem 22454 fmucndlem 22465 fsum2cn 23044 fimaproj 30445 curfv 33932 idfusubc0 42712 lmod1zr 43129 |
Copyright terms: Public domain | W3C validator |