![]() |
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 5738 | . 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
3 | reseqd.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | reseq2d 5739 | . 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
5 | 2, 4 | eqtrd 2831 | 1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 ↾ cres 5450 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rab 3114 df-v 3439 df-in 3870 df-opab 5029 df-xp 5454 df-res 5460 |
This theorem is referenced by: f1ossf1o 6758 tfrlem3a 7870 oieq1 8827 oieq2 8828 ackbij2lem3 9514 setsvalg 16346 resfval 16996 resfval2 16997 resf2nd 16999 lubfval 17422 glbfval 17435 dpjfval 18899 psrval 19835 znval 20369 prdsdsf 22665 prdsxmet 22667 imasdsf1olem 22671 xpsxmetlem 22677 xpsmet 22680 isxms 22745 isms 22747 setsxms 22777 setsms 22778 ressxms 22823 ressms 22824 prdsxmslem2 22827 cphsscph 23542 iscms 23636 cmsss 23642 cssbn 23666 minveclem3a 23718 dvcmulf 24230 efcvx 24725 issubgr 26741 ispth 27196 clwlknf1oclwwlkn 27555 eucrct2eupthOLD 27718 eucrct2eupth 27719 padct 30148 isrrext 30863 csbwrecsg 34164 prdsbnd2 34630 cnpwstotbnd 34632 ldualset 35817 dvmptresicc 41771 itgcoscmulx 41821 fourierdlem73 42032 sge0fodjrnlem 42266 vonval 42390 dfateq12d 42867 rngchomrnghmresALTV 43771 fdivval 44106 |
Copyright terms: Public domain | W3C validator |