![]() |
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 5984 | . 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
3 | reseqd.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | reseq2d 5985 | . 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
5 | 2, 4 | eqtrd 2765 | 1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ↾ cres 5680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-in 3951 df-opab 5212 df-xp 5684 df-res 5690 |
This theorem is referenced by: f1ossf1o 7137 csbfrecsg 8290 tfrlem3a 8398 oieq1 9537 oieq2 9538 ackbij2lem3 10266 setsvalg 17138 resfval 17881 resfval2 17882 resf2nd 17884 lubfval 18345 glbfval 18358 dpjfval 20024 znval 21482 psrval 21865 prdsdsf 24317 prdsxmet 24319 imasdsf1olem 24323 xpsxmetlem 24329 xpsmet 24332 isxms 24397 isms 24399 setsxms 24431 setsms 24432 ressxms 24478 ressms 24479 prdsxmslem2 24482 cphsscph 25223 iscms 25317 cmsss 25323 cssbn 25347 minveclem3a 25399 dvmptresicc 25889 dvcmulf 25920 efcvx 26431 issubgr 29156 ispth 29609 clwlknf1oclwwlkn 29966 eucrct2eupth 30127 padct 32583 isrrext 33732 prdsbnd2 37399 cnpwstotbnd 37401 ldualset 38727 itgcoscmulx 45495 fourierdlem73 45705 sge0fodjrnlem 45942 vonval 46066 dfateq12d 46644 isisubgr 47334 rngchomrnghmresALTV 47527 fdivval 47798 |
Copyright terms: Public domain | W3C validator |