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 5890 | . 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
3 | reseqd.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | reseq2d 5891 | . 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
5 | 2, 4 | eqtrd 2778 | 1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ↾ cres 5591 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-in 3894 df-opab 5137 df-xp 5595 df-res 5601 |
This theorem is referenced by: f1ossf1o 7000 csbfrecsg 8100 tfrlem3a 8208 oieq1 9271 oieq2 9272 ackbij2lem3 9997 setsvalg 16867 resfval 17607 resfval2 17608 resf2nd 17610 lubfval 18068 glbfval 18081 dpjfval 19658 znval 20739 psrval 21118 prdsdsf 23520 prdsxmet 23522 imasdsf1olem 23526 xpsxmetlem 23532 xpsmet 23535 isxms 23600 isms 23602 setsxms 23634 setsms 23635 ressxms 23681 ressms 23682 prdsxmslem2 23685 cphsscph 24415 iscms 24509 cmsss 24515 cssbn 24539 minveclem3a 24591 dvmptresicc 25080 dvcmulf 25109 efcvx 25608 issubgr 27638 ispth 28091 clwlknf1oclwwlkn 28448 eucrct2eupth 28609 padct 31054 isrrext 31950 prdsbnd2 35953 cnpwstotbnd 35955 ldualset 37139 itgcoscmulx 43510 fourierdlem73 43720 sge0fodjrnlem 43954 vonval 44078 dfateq12d 44618 rngchomrnghmresALTV 45554 fdivval 45885 |
Copyright terms: Public domain | W3C validator |