Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reseq1 | Structured version Visualization version GIF version |
Description: Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
reseq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 4178 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5560 | . 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
3 | df-res 5560 | . 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
4 | 1, 2, 3 | 3eqtr4g 2878 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 Vcvv 3492 ∩ cin 3932 × cxp 5546 ↾ cres 5550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rab 3144 df-in 3940 df-res 5560 |
This theorem is referenced by: reseq1i 5842 reseq1d 5845 imaeq1 5917 fvtresfn 6763 wfrlem1 7943 wfrlem3a 7946 wfrlem15 7958 tfrlem12 8014 pmresg 8423 resixpfo 8488 mapunen 8674 fseqenlem1 9438 axdc3lem2 9861 axdc3lem4 9863 axdc 9931 hashf1lem1 13801 lo1eq 14913 rlimeq 14914 symgfixfo 18496 lspextmo 19757 evlseu 20224 mdetunilem3 21151 mdetunilem4 21152 mdetunilem9 21157 lmbr 21794 ptuncnv 22343 iscau 23806 plyexmo 24829 relogf1o 25077 eulerpartlemt 31528 eulerpartlemgv 31530 eulerpartlemn 31538 eulerpart 31539 bnj1385 32003 bnj66 32031 bnj1234 32182 bnj1326 32195 bnj1463 32224 iscvm 32403 trpredlem1 32963 trpredtr 32966 trpredmintr 32967 frrlem1 33020 frrlem13 33032 noprefixmo 33099 nosupno 33100 nosupdm 33101 nosupfv 33103 nosupres 33104 nosupbnd1lem1 33105 nosupbnd1lem3 33107 nosupbnd1lem5 33109 nosupbnd2 33113 mbfresfi 34819 eqfnun 34878 sdclem2 34898 isdivrngo 35109 mzpcompact2lem 39226 diophrw 39234 eldioph2lem1 39235 eldioph2lem2 39236 eldioph3 39241 diophin 39247 diophrex 39250 rexrabdioph 39269 2rexfrabdioph 39271 3rexfrabdioph 39272 4rexfrabdioph 39273 6rexfrabdioph 39274 7rexfrabdioph 39275 eldioph4b 39286 pwssplit4 39567 dvnprodlem1 42107 dvnprodlem3 42109 ismea 42610 isome 42653 |
Copyright terms: Public domain | W3C validator |