![]() |
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 4030 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5369 | . 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
3 | df-res 5369 | . 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
4 | 1, 2, 3 | 3eqtr4g 2839 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 Vcvv 3398 ∩ cin 3791 × cxp 5355 ↾ cres 5359 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-in 3799 df-res 5369 |
This theorem is referenced by: reseq1i 5640 reseq1d 5643 imaeq1 5717 fvtresfn 6546 wfrlem1 7698 wfrlem3a 7701 wfrlem15 7714 tfrlem12 7770 pmresg 8170 resixpfo 8234 mapunen 8419 fseqenlem1 9182 axdc3lem2 9610 axdc3lem4 9612 axdc 9680 hashf1lem1 13557 lo1eq 14711 rlimeq 14712 symgfixfo 18246 lspextmo 19455 evlseu 19916 mdetunilem3 20829 mdetunilem4 20830 mdetunilem9 20835 lmbr 21474 ptuncnv 22023 iscau 23486 plyexmo 24509 relogf1o 24754 eulerpartlemt 31035 eulerpartlemgv 31037 eulerpartlemn 31045 eulerpart 31046 bnj1385 31506 bnj66 31533 bnj1234 31684 bnj1326 31697 bnj1463 31726 iscvm 31844 trpredlem1 32319 trpredtr 32322 trpredmintr 32323 frrlem1 32373 noprefixmo 32441 nosupno 32442 nosupdm 32443 nosupfv 32445 nosupres 32446 nosupbnd1lem1 32447 nosupbnd1lem3 32449 nosupbnd1lem5 32451 nosupbnd2 32455 mbfresfi 34086 eqfnun 34146 sdclem2 34167 isdivrngo 34378 mzpcompact2lem 38284 diophrw 38292 eldioph2lem1 38293 eldioph2lem2 38294 eldioph3 38299 diophin 38306 diophrex 38309 rexrabdioph 38328 2rexfrabdioph 38330 3rexfrabdioph 38331 4rexfrabdioph 38332 6rexfrabdioph 38333 7rexfrabdioph 38334 eldioph4b 38345 pwssplit4 38628 dvnprodlem1 41099 dvnprodlem3 41101 ismea 41602 isome 41645 |
Copyright terms: Public domain | W3C validator |