![]() |
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 4201 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5684 | . 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
3 | df-res 5684 | . 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
4 | 1, 2, 3 | 3eqtr4g 2793 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 Vcvv 3470 ∩ cin 3944 × cxp 5670 ↾ cres 5674 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3429 df-in 3952 df-res 5684 |
This theorem is referenced by: reseq1i 5975 reseq1d 5978 imaeq1 6052 fvtresfn 7001 eqfnun 7040 frrlem1 8285 frrlem13 8297 wfrlem1OLD 8322 wfrlem3OLDa 8325 wfrlem15OLD 8337 tfrlem12 8403 pmresg 8882 resixpfo 8948 mapunen 9164 fseqenlem1 10041 axdc3lem2 10468 axdc3lem4 10470 axdc 10538 hashf1lem1 14441 hashf1lem1OLD 14442 lo1eq 15538 rlimeq 15539 symgfixfo 19387 lspextmo 20934 evlseu 22022 mdetunilem3 22509 mdetunilem4 22510 mdetunilem9 22515 lmbr 23155 ptuncnv 23704 iscau 25197 plyexmo 26241 relogf1o 26493 nosupprefixmo 27626 noinfprefixmo 27627 nosupcbv 27628 nosupno 27629 nosupdm 27630 nosupfv 27632 nosupres 27633 nosupbnd1lem1 27634 nosupbnd1lem3 27636 nosupbnd1lem5 27638 nosupbnd2 27642 noinfcbv 27643 noinfno 27644 noinfdm 27645 noinffv 27647 noinfres 27648 noinfbnd1lem1 27649 noinfbnd1lem3 27651 noinfbnd1lem5 27653 noinfbnd2 27657 eulerpartlemt 33985 eulerpartlemgv 33987 eulerpartlemn 33995 eulerpart 33996 bnj1385 34457 bnj66 34485 bnj1234 34638 bnj1326 34651 bnj1463 34680 iscvm 34863 mbfresfi 37133 sdclem2 37209 isdivrngo 37417 evlselvlem 41813 evlselv 41814 mzpcompact2lem 42165 diophrw 42173 eldioph2lem1 42174 eldioph2lem2 42175 eldioph3 42180 diophin 42186 diophrex 42189 rexrabdioph 42208 2rexfrabdioph 42210 3rexfrabdioph 42211 4rexfrabdioph 42212 6rexfrabdioph 42213 7rexfrabdioph 42214 eldioph4b 42225 pwssplit4 42507 dvnprodlem1 45328 dvnprodlem3 45330 ismea 45833 isome 45876 |
Copyright terms: Public domain | W3C validator |