|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > reseq12d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.) | 
| Ref | Expression | 
|---|---|
| reseqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) | 
| reseqd.2 | ⊢ (𝜑 → 𝐶 = 𝐷) | 
| Ref | Expression | 
|---|---|
| reseq12d | ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | reseqd.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | 1 | reseq1d 5996 | . 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | 
| 3 | reseqd.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
| 4 | 3 | reseq2d 5997 | . 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷)) | 
| 5 | 2, 4 | eqtrd 2777 | 1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1540 ↾ 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: f1ossf1o 7148 csbfrecsg 8309 tfrlem3a 8417 oieq1 9552 oieq2 9553 ackbij2lem3 10280 setsvalg 17203 resfval 17937 resfval2 17938 resf2nd 17940 lubfval 18395 glbfval 18408 dpjfval 20075 znval 21550 psrval 21935 prdsdsf 24377 prdsxmet 24379 imasdsf1olem 24383 xpsxmetlem 24389 xpsmet 24392 isxms 24457 isms 24459 setsxms 24491 setsms 24492 ressxms 24538 ressms 24539 prdsxmslem2 24542 cphsscph 25285 iscms 25379 cmsss 25385 cssbn 25409 minveclem3a 25461 dvmptresicc 25951 dvcmulf 25982 efcvx 26493 issubgr 29288 ispth 29741 clwlknf1oclwwlkn 30103 eucrct2eupth 30264 padct 32731 isrrext 34001 prdsbnd2 37802 cnpwstotbnd 37804 ldualset 39126 itgcoscmulx 45984 fourierdlem73 46194 sge0fodjrnlem 46431 vonval 46555 dfateq12d 47138 isisubgr 47848 rngchomrnghmresALTV 48195 fdivval 48460 | 
| Copyright terms: Public domain | W3C validator |