Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reseq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
reseq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 3807 | . 2 | |
2 | df-res 5126 | . 2 | |
3 | df-res 5126 | . 2 | |
4 | 1, 2, 3 | 3eqtr4g 2681 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cvv 3200 cin 3573 cxp 5112 cres 5116 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-res 5126 |
This theorem is referenced by: reseq1i 5392 reseq1d 5395 imaeq1 5461 fvtresfn 6284 wfrlem1 7414 wfrlem3a 7417 wfrlem15 7429 tfrlem12 7485 pmresg 7885 resixpfo 7946 mapunen 8129 fseqenlem1 8847 axdc3lem2 9273 axdc3lem4 9275 axdc 9343 hashf1lem1 13239 lo1eq 14299 rlimeq 14300 symgfixfo 17859 lspextmo 19056 evlseu 19516 mdetunilem3 20420 mdetunilem4 20421 mdetunilem9 20426 lmbr 21062 ptuncnv 21610 iscau 23074 plyexmo 24068 relogf1o 24313 eulerpartlemt 30433 eulerpartlemgv 30435 eulerpartlemn 30443 eulerpart 30444 bnj1385 30903 bnj66 30930 bnj1234 31081 bnj1326 31094 bnj1463 31123 iscvm 31241 trpredlem1 31727 trpredtr 31730 trpredmintr 31731 frrlem1 31780 noprefixmo 31848 nosupno 31849 nosupdm 31850 nosupfv 31852 nosupres 31853 nosupbnd1lem1 31854 nosupbnd1lem3 31856 nosupbnd1lem5 31858 nosupbnd2 31862 mbfresfi 33456 eqfnun 33516 sdclem2 33538 isdivrngo 33749 mzpcompact2lem 37314 diophrw 37322 eldioph2lem1 37323 eldioph2lem2 37324 eldioph3 37329 diophin 37336 diophrex 37339 rexrabdioph 37358 2rexfrabdioph 37360 3rexfrabdioph 37361 4rexfrabdioph 37362 6rexfrabdioph 37363 7rexfrabdioph 37364 eldioph4b 37375 pwssplit4 37659 dvnprodlem1 40161 dvnprodlem3 40163 ismea 40668 isome 40708 |
Copyright terms: Public domain | W3C validator |