![]() |
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 5690 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V)) | |
2 | 1 | ineq2d 4212 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V))) |
3 | df-res 5688 | . 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V)) | |
4 | df-res 5688 | . 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V)) | |
5 | 2, 3, 4 | 3eqtr4g 2798 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 Vcvv 3475 ∩ cin 3947 × cxp 5674 ↾ cres 5678 |
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 3955 df-opab 5211 df-xp 5682 df-res 5688 |
This theorem is referenced by: reseq2i 5977 reseq2d 5980 resabs1 6010 resima2 6015 reldisjun 6031 imaeq2 6054 resdisj 6166 dfpo2 6293 fimadmfoALT 6814 fressnfv 7155 tfrlem1 8373 tfrlem9 8382 tfrlem11 8385 tfrlem12 8386 tfr2b 8393 tz7.44-1 8403 tz7.44-2 8404 tz7.44-3 8405 rdglem1 8412 fnfi 9178 fseqenlem1 10016 rtrclreclem4 15005 psgnprfval1 19385 gsumzaddlem 19784 gsum2dlem2 19834 znunithash 21112 islinds 21356 lmbr2 22755 lmff 22797 kgencn2 23053 ptcmpfi 23309 tsmsgsum 23635 tsmsres 23640 tsmsf1o 23641 tsmsxplem1 23649 tsmsxp 23651 ustval 23699 xrge0gsumle 24341 xrge0tsms 24342 lmmbr2 24768 lmcau 24822 limcun 25404 jensen 26483 wilthlem2 26563 wilthlem3 26564 hhssnvt 30506 hhsssh 30510 foresf1o 31730 xrge0tsmsd 32197 gsumle 32230 esumsnf 33051 subfacp1lem3 34162 subfacp1lem5 34164 erdszelem1 34171 erdsze 34182 erdsze2lem2 34184 cvmscbv 34238 cvmshmeo 34251 cvmsss2 34254 eldm3 34720 dfrdg2 34756 bj-diagval 36044 mbfresfi 36523 disjresin 37095 elcoeleqvrels 37454 eleldisjs 37587 eldisjeq 37600 eqvrelqseqdisj3 37690 mzpcompact2lem 41475 seff 43054 wessf1ornlem 43868 fouriersw 44934 sge0tsms 45083 sge0f1o 45085 sge0sup 45094 meadjuni 45160 ismeannd 45170 psmeasurelem 45173 psmeasure 45174 omeunile 45208 isomennd 45234 hoidmvlelem3 45300 |
Copyright terms: Public domain | W3C validator |