Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reseq2 | Structured version Visualization version GIF version |
Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.) |
Ref | Expression |
---|---|
reseq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1 5603 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V)) | |
2 | 1 | ineq2d 4146 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V))) |
3 | df-res 5601 | . 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V)) | |
4 | df-res 5601 | . 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V)) | |
5 | 2, 3, 4 | 3eqtr4g 2803 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 Vcvv 3432 ∩ cin 3886 × cxp 5587 ↾ cres 5591 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-in 3894 df-opab 5137 df-xp 5595 df-res 5601 |
This theorem is referenced by: reseq2i 5888 reseq2d 5891 resabs1 5921 resima2 5926 imaeq2 5965 resdisj 6072 dfpo2 6199 fimadmfoALT 6699 fressnfv 7032 tfrlem1 8207 tfrlem9 8216 tfrlem11 8219 tfrlem12 8220 tfr2b 8227 tz7.44-1 8237 tz7.44-2 8238 tz7.44-3 8239 rdglem1 8246 fnfi 8964 fseqenlem1 9780 rtrclreclem4 14772 psgnprfval1 19130 gsumzaddlem 19522 gsum2dlem2 19572 znunithash 20772 islinds 21016 lmbr2 22410 lmff 22452 kgencn2 22708 ptcmpfi 22964 tsmsgsum 23290 tsmsres 23295 tsmsf1o 23296 tsmsxplem1 23304 tsmsxp 23306 ustval 23354 xrge0gsumle 23996 xrge0tsms 23997 lmmbr2 24423 lmcau 24477 limcun 25059 jensen 26138 wilthlem2 26218 wilthlem3 26219 hhssnvt 29627 hhsssh 29631 foresf1o 30850 reldisjun 30942 xrge0tsmsd 31317 gsumle 31350 esumsnf 32032 subfacp1lem3 33144 subfacp1lem5 33146 erdszelem1 33153 erdsze 33164 erdsze2lem2 33166 cvmscbv 33220 cvmshmeo 33233 cvmsss2 33236 eldm3 33728 dfrdg2 33771 bj-diagval 35345 mbfresfi 35823 elcoeleqvrels 36708 eleldisjs 36839 eldisjeq 36852 mzpcompact2lem 40573 seff 41927 wessf1ornlem 42722 fouriersw 43772 sge0tsms 43918 sge0f1o 43920 sge0sup 43929 meadjuni 43995 ismeannd 44005 psmeasurelem 44008 psmeasure 44009 omeunile 44043 isomennd 44069 hoidmvlelem3 44135 |
Copyright terms: Public domain | W3C validator |