![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reseq2i | Structured version Visualization version GIF version |
Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
reseqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
reseq2i | ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | reseq2 5974 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ↾ cres 5677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-in 3954 df-opab 5210 df-xp 5681 df-res 5687 |
This theorem is referenced by: reseq12i 5977 rescom 6005 resdmdfsn 6029 idinxpresid 6045 rescnvcnv 6200 resdm2 6227 funcnvres 6623 resasplit 6758 fresaunres2 6760 fresaunres1 6761 resdif 6851 resin 6852 funcocnv2 6855 fvn0ssdmfun 7072 residpr 7136 eqfunressuc 7353 fprlem1 8280 wfrlem5OLD 8308 domss2 9132 ordtypelem1 9509 frrlem15 9748 ackbij2lem3 10232 facnn 14231 fac0 14232 hashresfn 14296 relexpcnv 14978 divcnvshft 15797 ruclem4 16173 fsets 17098 setsid 17137 join0 18354 meet0 18355 symgfixelsi 19296 psgnsn 19381 dprd2da 19904 ply1plusgfvi 21746 uptx 23111 txcn 23112 ressxms 24016 ressms 24017 iscmet3lem3 24789 volres 25027 dvlip 25492 dvne0 25510 lhop 25515 dflog2 26051 dfrelog 26056 dvlog 26141 wilthlem2 26553 nosupbnd2lem1 27198 noinfbnd2lem1 27213 0grsubgr 28515 0pth 29358 1pthdlem1 29368 eupth2lemb 29470 ex-fpar 29695 fressupp 31888 df1stres 31903 df2ndres 31904 ffsrn 31932 resf1o 31933 fpwrelmapffs 31937 cycpmconjv 32279 sitmcl 33288 eulerpartlemn 33318 bnj1326 33975 satfv1lem 34291 divcnvlin 34640 poimirlem9 36435 zrdivrng 36759 isdrngo1 36762 ressucdifsn 37049 cnvresrn 37155 disjsuc 37567 eldioph4b 41482 diophren 41484 rclexi 42299 rtrclex 42301 cnvrcl0 42309 dfrtrcl5 42313 dfrcl2 42358 relexpiidm 42388 relexp01min 42397 relexpaddss 42402 seff 43001 sblpnf 43002 radcnvrat 43006 hashnzfzclim 43014 dvresioo 44572 fourierdlem72 44829 fourierdlem80 44837 fourierdlem94 44851 fourierdlem103 44860 fourierdlem104 44861 fourierdlem113 44870 fouriersw 44882 sge0split 45060 rngcidALTV 46791 ringcidALTV 46854 |
Copyright terms: Public domain | W3C validator |