Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resmpt | Structured version Visualization version GIF version |
Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.) |
Ref | Expression |
---|---|
resmpt | ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resopab2 5898 | . 2 ⊢ (𝐵 ⊆ 𝐴 → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)}) | |
2 | df-mpt 5139 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} | |
3 | 2 | reseq1i 5843 | . 2 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵) |
4 | df-mpt 5139 | . 2 ⊢ (𝑥 ∈ 𝐵 ↦ 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)} | |
5 | 1, 3, 4 | 3eqtr4g 2881 | 1 ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ⊆ wss 3935 {copab 5120 ↦ cmpt 5138 ↾ cres 5551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-opab 5121 df-mpt 5139 df-xp 5555 df-rel 5556 df-res 5561 |
This theorem is referenced by: resmpt3 5900 resmptf 5901 resmptd 5902 mptss 5904 fvresex 7652 f1stres 7704 f2ndres 7705 tposss 7884 dftpos2 7900 dftpos4 7902 resixpfo 8489 rlimresb 14912 lo1eq 14915 rlimeq 14916 fsumss 15072 isumclim3 15104 divcnvshft 15200 fprodss 15292 iprodclim3 15344 fprodefsum 15438 bitsf1ocnv 15783 conjsubg 18330 odf1o2 18629 sylow1lem2 18655 sylow2blem1 18676 gsumzres 18960 gsumzsplit 18978 gsumpr 19006 gsumzunsnd 19007 gsum2dlem2 19022 gsummptnn0fz 19037 dprd2da 19095 dpjidcl 19111 ablfac1b 19123 psrass1lem 20087 coe1mul2lem2 20366 frlmsplit2 20847 ofco2 20990 mdetralt 21147 mdetunilem9 21159 tgrest 21697 cmpfi 21946 fmss 22484 txflf 22544 tmdgsum 22633 tgpconncomp 22650 tsmssplit 22689 iscmet3lem3 23822 mbfss 24176 mbfadd 24191 mbfsub 24192 mbflimsup 24196 mbfmul 24256 itg2cnlem1 24291 ellimc2 24404 dvreslem 24436 dvres2lem 24437 dvidlem 24442 dvcnp2 24446 dvmulbr 24465 dvcobr 24472 dvrec 24481 dvmptntr 24497 dvcnvlem 24502 lhop1lem 24539 lhop2 24541 itgparts 24573 itgsubstlem 24574 tdeglem4 24583 plypf1 24731 taylthlem2 24891 pserdvlem2 24945 abelth 24958 pige3ALT 25034 efifo 25058 eff1olem 25059 dvlog2 25163 resqrtcn 25257 sqrtcn 25258 dvatan 25440 rlimcnp2 25472 xrlimcnp 25474 efrlim 25475 cxp2lim 25482 chpo1ub 25984 dchrisum0lem2a 26021 pnt2 26117 pnt 26118 wlknwwlksnbij 27594 elimampt 30312 ressnm 30566 gsummpt2d 30615 rmulccn 31071 xrge0mulc1cn 31084 gsumesum 31218 esumsnf 31223 esumcvg 31245 omsmon 31456 carsggect 31476 eulerpartlem1 31525 eulerpartgbij 31530 gsumnunsn 31711 cxpcncf1 31766 itgexpif 31777 reprpmtf1o 31797 elmsubrn 32673 divcnvlin 32862 mptsnunlem 34502 dissneqlem 34504 broucube 34808 mbfposadd 34821 itggt0cn 34846 ftc1anclem3 34851 ftc1anclem8 34856 dvasin 34860 dvacos 34861 areacirc 34869 sdclem2 34900 cncfres 34926 pwssplit4 39569 pwfi2f1o 39576 hbtlem6 39609 itgpowd 39701 areaquad 39703 hashnzfzclim 40534 lhe4.4ex1a 40541 resmpti 41314 climresmpt 41820 dvcosre 42076 dvmptresicc 42084 itgsinexplem1 42119 itgcoscmulx 42134 dirkeritg 42268 dirkercncflem2 42270 fourierdlem16 42289 fourierdlem21 42294 fourierdlem22 42295 fourierdlem57 42329 fourierdlem58 42330 fourierdlem62 42334 fourierdlem83 42355 fourierdlem111 42383 fouriersw 42397 0ome 42692 |
Copyright terms: Public domain | W3C validator |