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 5316 | . 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
3 | reseqd.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | reseq2d 5317 | . 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
5 | 2, 4 | eqtrd 2644 | 1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ↾ cres 5040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-opab 4644 df-xp 5044 df-res 5050 |
This theorem is referenced by: tfrlem3a 7360 oieq1 8300 oieq2 8301 ackbij2lem3 8946 setsvalg 15719 resfval 16375 resfval2 16376 resf2nd 16378 lubfval 16801 glbfval 16814 dpjfval 18277 psrval 19183 znval 19702 prdsdsf 21982 prdsxmet 21984 imasdsf1olem 21988 xpsxmetlem 21994 xpsmet 21997 isxms 22062 isms 22064 setsxms 22094 setsms 22095 ressxms 22140 ressms 22141 prdsxmslem2 22144 iscms 22950 cmsss 22955 minveclem3a 23006 dvcmulf 23514 efcvx 24007 ispth 26098 constr3pthlem1 26183 padct 28885 isrrext 29372 csbwrecsg 32349 prdsbnd2 32764 cnpwstotbnd 32766 ldualset 33430 dvmptresicc 38809 itgcoscmulx 38861 fourierdlem73 39072 sge0fodjrnlem 39309 vonval 39430 dfateq12d 39858 issubgr 40495 isPth 40929 eucrct2eupth 41413 rngchomrnghmresALTV 41788 fdivval 42131 |
Copyright terms: Public domain | W3C validator |