![]() |
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 5652 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V)) | |
2 | 1 | ineq2d 4177 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V))) |
3 | df-res 5650 | . 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V)) | |
4 | df-res 5650 | . 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V)) | |
5 | 2, 3, 4 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 Vcvv 3448 ∩ cin 3914 × cxp 5636 ↾ cres 5640 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-in 3922 df-opab 5173 df-xp 5644 df-res 5650 |
This theorem is referenced by: reseq2i 5939 reseq2d 5942 resabs1 5972 resima2 5977 imaeq2 6014 resdisj 6126 dfpo2 6253 fimadmfoALT 6772 fressnfv 7111 tfrlem1 8327 tfrlem9 8336 tfrlem11 8339 tfrlem12 8340 tfr2b 8347 tz7.44-1 8357 tz7.44-2 8358 tz7.44-3 8359 rdglem1 8366 fnfi 9132 fseqenlem1 9967 rtrclreclem4 14953 psgnprfval1 19311 gsumzaddlem 19705 gsum2dlem2 19755 znunithash 20987 islinds 21231 lmbr2 22626 lmff 22668 kgencn2 22924 ptcmpfi 23180 tsmsgsum 23506 tsmsres 23511 tsmsf1o 23512 tsmsxplem1 23520 tsmsxp 23522 ustval 23570 xrge0gsumle 24212 xrge0tsms 24213 lmmbr2 24639 lmcau 24693 limcun 25275 jensen 26354 wilthlem2 26434 wilthlem3 26435 hhssnvt 30249 hhsssh 30253 foresf1o 31473 reldisjun 31563 xrge0tsmsd 31941 gsumle 31974 esumsnf 32703 subfacp1lem3 33816 subfacp1lem5 33818 erdszelem1 33825 erdsze 33836 erdsze2lem2 33838 cvmscbv 33892 cvmshmeo 33905 cvmsss2 33908 eldm3 34373 dfrdg2 34409 bj-diagval 35674 mbfresfi 36153 disjresin 36726 elcoeleqvrels 37086 eleldisjs 37219 eldisjeq 37232 eqvrelqseqdisj3 37322 mzpcompact2lem 41103 seff 42663 wessf1ornlem 43477 fouriersw 44546 sge0tsms 44695 sge0f1o 44697 sge0sup 44706 meadjuni 44772 ismeannd 44782 psmeasurelem 44785 psmeasure 44786 omeunile 44820 isomennd 44846 hoidmvlelem3 44912 |
Copyright terms: Public domain | W3C validator |