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 5533 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V)) | |
2 | 1 | ineq2d 4101 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V))) |
3 | df-res 5531 | . 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V)) | |
4 | df-res 5531 | . 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V)) | |
5 | 2, 3, 4 | 3eqtr4g 2798 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 Vcvv 3397 ∩ cin 3840 × cxp 5517 ↾ cres 5521 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-in 3848 df-opab 5090 df-xp 5525 df-res 5531 |
This theorem is referenced by: reseq2i 5816 reseq2d 5819 resabs1 5849 resima2 5854 imaeq2 5893 resdisj 5995 fimadmfoALT 6597 fressnfv 6926 tfrlem1 8034 tfrlem9 8043 tfrlem11 8046 tfrlem12 8047 tfr2b 8054 tz7.44-1 8064 tz7.44-2 8065 tz7.44-3 8066 rdglem1 8073 fnfi 8771 fseqenlem1 9517 rtrclreclem4 14503 psgnprfval1 18761 gsumzaddlem 19153 gsum2dlem2 19203 znunithash 20376 islinds 20618 lmbr2 22003 lmff 22045 kgencn2 22301 ptcmpfi 22557 tsmsgsum 22883 tsmsres 22888 tsmsf1o 22889 tsmsxplem1 22897 tsmsxp 22899 ustval 22947 xrge0gsumle 23578 xrge0tsms 23579 lmmbr2 24004 lmcau 24058 limcun 24639 jensen 25718 wilthlem2 25798 wilthlem3 25799 hhssnvt 29192 hhsssh 29196 foresf1o 30416 reldisjun 30508 xrge0tsmsd 30886 gsumle 30919 esumsnf 31594 subfacp1lem3 32707 subfacp1lem5 32709 erdszelem1 32716 erdsze 32727 erdsze2lem2 32729 cvmscbv 32783 cvmshmeo 32796 cvmsss2 32799 dfpo2 33286 eldm3 33292 dfrdg2 33335 bj-diagval 34955 mbfresfi 35435 elcoeleqvrels 36320 eleldisjs 36451 eldisjeq 36464 mzpcompact2lem 40129 seff 41449 wessf1ornlem 42244 fouriersw 43298 sge0tsms 43444 sge0f1o 43446 sge0sup 43455 meadjuni 43521 ismeannd 43531 psmeasurelem 43534 psmeasure 43535 omeunile 43569 isomennd 43595 hoidmvlelem3 43661 |
Copyright terms: Public domain | W3C validator |