Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reseq12i | Structured version Visualization version GIF version |
Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
Ref | Expression |
---|---|
reseqi.1 | ⊢ 𝐴 = 𝐵 |
reseqi.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
reseq12i | ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseqi.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 1 | reseq1i 5886 | . 2 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶) |
3 | reseqi.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
4 | 3 | reseq2i 5887 | . 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷) |
5 | 2, 4 | eqtri 2768 | 1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ↾ cres 5592 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1545 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-rab 3075 df-in 3899 df-opab 5142 df-xp 5596 df-res 5602 |
This theorem is referenced by: cnvresid 6511 fprlem1 8107 wfrlem5OLD 8135 dfoi 9248 frrlem15 9516 lubfval 18066 glbfval 18079 odulub 18123 oduglb 18125 dvlog 25804 dvlog2 25806 issubgr 27636 finsumvtxdg2size 27915 sitgclg 32305 fourierdlem57 43675 fourierdlem74 43692 fourierdlem75 43693 |
Copyright terms: Public domain | W3C validator |