![]() |
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 4170 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5650 | . 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
3 | df-res 5650 | . 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
4 | 1, 2, 3 | 3eqtr4g 2796 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 Vcvv 3446 ∩ cin 3912 × cxp 5636 ↾ cres 5640 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3406 df-in 3920 df-res 5650 |
This theorem is referenced by: reseq1i 5938 reseq1d 5941 imaeq1 6013 fvtresfn 6955 frrlem1 8222 frrlem13 8234 wfrlem1OLD 8259 wfrlem3OLDa 8262 wfrlem15OLD 8274 tfrlem12 8340 pmresg 8815 resixpfo 8881 mapunen 9097 fseqenlem1 9969 axdc3lem2 10396 axdc3lem4 10398 axdc 10466 hashf1lem1 14365 hashf1lem1OLD 14366 lo1eq 15462 rlimeq 15463 symgfixfo 19235 lspextmo 20574 evlseu 21530 mdetunilem3 22000 mdetunilem4 22001 mdetunilem9 22006 lmbr 22646 ptuncnv 23195 iscau 24677 plyexmo 25710 relogf1o 25959 nosupprefixmo 27085 noinfprefixmo 27086 nosupcbv 27087 nosupno 27088 nosupdm 27089 nosupfv 27091 nosupres 27092 nosupbnd1lem1 27093 nosupbnd1lem3 27095 nosupbnd1lem5 27097 nosupbnd2 27101 noinfcbv 27102 noinfno 27103 noinfdm 27104 noinffv 27106 noinfres 27107 noinfbnd1lem1 27108 noinfbnd1lem3 27110 noinfbnd1lem5 27112 noinfbnd2 27116 eulerpartlemt 33060 eulerpartlemgv 33062 eulerpartlemn 33070 eulerpart 33071 bnj1385 33533 bnj66 33561 bnj1234 33714 bnj1326 33727 bnj1463 33756 iscvm 33940 mbfresfi 36197 eqfnun 36254 sdclem2 36274 isdivrngo 36482 mzpcompact2lem 41132 diophrw 41140 eldioph2lem1 41141 eldioph2lem2 41142 eldioph3 41147 diophin 41153 diophrex 41156 rexrabdioph 41175 2rexfrabdioph 41177 3rexfrabdioph 41178 4rexfrabdioph 41179 6rexfrabdioph 41180 7rexfrabdioph 41181 eldioph4b 41192 pwssplit4 41474 dvnprodlem1 44307 dvnprodlem3 44309 ismea 44812 isome 44855 |
Copyright terms: Public domain | W3C validator |