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 3769 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5050 | . 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
3 | df-res 5050 | . 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
4 | 1, 2, 3 | 3eqtr4g 2669 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 Vcvv 3173 ∩ cin 3539 × cxp 5036 ↾ cres 5040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-res 5050 |
This theorem is referenced by: reseq1i 5313 reseq1d 5316 imaeq1 5380 fvtresfn 6193 wfrlem1 7301 wfrlem3a 7304 wfrlem15 7316 tfrlem12 7372 pmresg 7771 resixpfo 7832 mapunen 8014 fseqenlem1 8730 axdc3lem2 9156 axdc3lem4 9158 axdc 9226 hashf1lem1 13096 lo1eq 14147 rlimeq 14148 symgfixfo 17682 lspextmo 18877 evlseu 19337 mdetunilem3 20239 mdetunilem4 20240 mdetunilem9 20245 lmbr 20872 ptuncnv 21420 iscau 22882 plyexmo 23872 relogf1o 24117 eulerpartlemt 29760 eulerpartlemgv 29762 eulerpartlemn 29770 eulerpart 29771 bnj1385 30157 bnj66 30184 bnj1234 30335 bnj1326 30348 bnj1463 30377 iscvm 30495 trpredlem1 30971 trpredtr 30974 trpredmintr 30975 frrlem1 31024 nofulllem5 31105 mbfresfi 32626 eqfnun 32686 sdclem2 32708 isdivrngo 32919 mzpcompact2lem 36332 diophrw 36340 eldioph2lem1 36341 eldioph2lem2 36342 eldioph3 36347 diophin 36354 diophrex 36357 rexrabdioph 36376 2rexfrabdioph 36378 3rexfrabdioph 36379 4rexfrabdioph 36380 6rexfrabdioph 36381 7rexfrabdioph 36382 eldioph4b 36393 pwssplit4 36677 dvnprodlem1 38836 dvnprodlem3 38838 ismea 39344 isome 39384 |
Copyright terms: Public domain | W3C validator |