![]() |
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 3639 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-res 4865 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-res 4865 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3eqtr4g 2521 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-in 3423 df-res 4865 |
This theorem is referenced by: reseq1i 5120 reseq1d 5123 imaeq1 5182 relcoi1OLD 5384 fvtresfn 5973 wfrlem1 7061 wfrlem3a 7064 wfrlem15 7076 tfrlem12 7133 pmresg 7525 resixpfo 7586 mapunen 7767 fseqenlem1 8481 axdc3lem2 8907 axdc3lem4 8909 axdc 8977 hashf1lem1 12651 lo1eq 13681 rlimeq 13682 symgfixfo 17129 lspextmo 18328 evlseu 18788 mdetunilem3 19688 mdetunilem4 19689 mdetunilem9 19694 lmbr 20323 ptuncnv 20871 iscau 22295 plyexmo 23315 relogf1o 23565 isdivrngo 26208 eulerpartlemt 29253 eulerpartlemgv 29255 eulerpartlemn 29263 eulerpart 29264 bnj1385 29693 bnj66 29720 bnj1234 29871 bnj1326 29884 bnj1463 29913 iscvm 30031 ghomgrplem 30356 trpredlem1 30517 trpredtr 30520 trpredmintr 30521 frrlem1 30563 nofulllem5 30644 mbfresfi 32032 eqfnun 32093 sdclem2 32116 mzpcompact2lem 35638 diophrw 35646 eldioph2lem1 35647 eldioph2lem2 35648 eldioph3 35653 diophin 35660 diophrex 35663 rexrabdioph 35682 2rexfrabdioph 35684 3rexfrabdioph 35685 4rexfrabdioph 35686 6rexfrabdioph 35687 7rexfrabdioph 35688 eldioph4b 35699 pwssplit4 35992 dvnprodlem1 37859 dvnprodlem3 37861 ismea 38327 isome 38353 |
Copyright terms: Public domain | W3C validator |