| 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 4213 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V))) | |
| 2 | df-res 5697 | . 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
| 3 | df-res 5697 | . 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
| 4 | 1, 2, 3 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 Vcvv 3480 ∩ cin 3950 × cxp 5683 ↾ cres 5687 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-in 3958 df-res 5697 |
| This theorem is referenced by: reseq1i 5993 reseq1d 5996 imaeq1 6073 fvtresfn 7018 eqfnun 7057 frrlem1 8311 frrlem13 8323 wfrlem1OLD 8348 wfrlem3OLDa 8351 wfrlem15OLD 8363 tfrlem12 8429 pmresg 8910 resixpfo 8976 mapunen 9186 fseqenlem1 10064 axdc3lem2 10491 axdc3lem4 10493 hashf1lem1 14494 lo1eq 15604 rlimeq 15605 symgfixfo 19457 lspextmo 21055 evlseu 22107 mdetunilem3 22620 mdetunilem4 22621 mdetunilem9 22626 lmbr 23266 ptuncnv 23815 iscau 25310 plyexmo 26355 relogf1o 26608 nosupprefixmo 27745 noinfprefixmo 27746 nosupcbv 27747 nosupno 27748 nosupdm 27749 nosupfv 27751 nosupres 27752 nosupbnd1lem1 27753 nosupbnd1lem3 27755 nosupbnd1lem5 27757 nosupbnd2 27761 noinfcbv 27762 noinfno 27763 noinfdm 27764 noinffv 27766 noinfres 27767 noinfbnd1lem1 27768 noinfbnd1lem3 27770 noinfbnd1lem5 27772 noinfbnd2 27776 eulerpartlemt 34373 eulerpartlemgv 34375 eulerpartlemn 34383 eulerpart 34384 bnj1385 34846 bnj66 34874 bnj1234 35027 bnj1326 35040 bnj1463 35069 iscvm 35264 mbfresfi 37673 sdclem2 37749 isdivrngo 37957 evlselvlem 42596 evlselv 42597 mzpcompact2lem 42762 diophrw 42770 eldioph2lem1 42771 eldioph2lem2 42772 eldioph3 42777 diophin 42783 diophrex 42786 rexrabdioph 42805 2rexfrabdioph 42807 3rexfrabdioph 42808 4rexfrabdioph 42809 6rexfrabdioph 42810 7rexfrabdioph 42811 eldioph4b 42822 pwssplit4 43101 dvnprodlem1 45961 dvnprodlem3 45963 ismea 46466 isome 46509 |
| Copyright terms: Public domain | W3C validator |