| 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 5699 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V)) | |
| 2 | 1 | ineq2d 4220 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V))) |
| 3 | df-res 5697 | . 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V)) | |
| 4 | df-res 5697 | . 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V)) | |
| 5 | 2, 3, 4 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 Vcvv 3480 ∩ cin 3950 × cxp 5683 ↾ cres 5687 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-in 3958 df-opab 5206 df-xp 5691 df-res 5697 |
| This theorem is referenced by: reseq2i 5994 reseq2d 5997 resabs1 6024 resima2 6034 reldisjun 6050 imaeq2 6074 resdisj 6189 dfpo2 6316 fimadmfoALT 6831 fressnfv 7180 tfrlem1 8416 tfrlem9 8425 tfrlem11 8428 tfrlem12 8429 tfr2b 8436 tz7.44-1 8446 tz7.44-2 8447 tz7.44-3 8448 rdglem1 8455 fnfi 9218 fseqenlem1 10064 rtrclreclem4 15100 psgnprfval1 19540 gsumzaddlem 19939 gsum2dlem2 19989 znunithash 21583 islinds 21829 lmbr2 23267 lmff 23309 kgencn2 23565 ptcmpfi 23821 tsmsgsum 24147 tsmsres 24152 tsmsf1o 24153 tsmsxplem1 24161 tsmsxp 24163 ustval 24211 xrge0gsumle 24855 xrge0tsms 24856 lmmbr2 25293 lmcau 25347 limcun 25930 jensen 27032 wilthlem2 27112 wilthlem3 27113 hhssnvt 31284 hhsssh 31288 foresf1o 32523 xrge0tsmsd 33065 gsumle 33101 rprmdvdsprod 33562 esumsnf 34065 subfacp1lem3 35187 subfacp1lem5 35189 erdszelem1 35196 erdsze 35207 erdsze2lem2 35209 cvmscbv 35263 cvmshmeo 35276 cvmsss2 35279 eldm3 35761 dfrdg2 35796 bj-diagval 37175 mbfresfi 37673 disjresin 38241 elcoeleqvrels 38596 eleldisjs 38729 eldisjeq 38742 eqvrelqseqdisj3 38832 mzpcompact2lem 42762 seff 44328 wessf1ornlem 45190 fouriersw 46246 sge0tsms 46395 sge0f1o 46397 sge0sup 46406 meadjuni 46472 ismeannd 46482 psmeasurelem 46485 psmeasure 46486 omeunile 46520 isomennd 46546 hoidmvlelem3 46612 |
| Copyright terms: Public domain | W3C validator |