![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmres | Structured version Visualization version Unicode version |
Description: The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
dmres |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3050 |
. . . . 5
![]() ![]() ![]() ![]() | |
2 | 1 | eldm2 5036 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 19.41v 1832 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | vex 3050 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
5 | 4 | opelres 5113 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | exbii 1720 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1 | eldm2 5036 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | anbi1i 702 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 6, 8 | 3bitr4i 281 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 2, 9 | bitr2i 254 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10 | ineqri 3628 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | incom 3627 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 11, 12 | eqtr3i 2477 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-br 4406 df-opab 4465 df-xp 4843 df-dm 4847 df-res 4849 |
This theorem is referenced by: ssdmres 5129 dmresexg 5130 dmressnsn 5146 eldmeldmressn 5148 imadisj 5190 ndmimaOLD 5209 imainrect 5281 dmresv 5297 resdmres 5329 coeq0 5347 funimacnv 5660 fnresdisj 5691 fnres 5697 fresaunres2 5760 nfvres 5900 ssimaex 5935 fnreseql 5997 respreima 6014 fveqressseq 6023 ffvresb 6059 fsnunfv 6109 funfvima 6145 funiunfv 6158 offres 6793 fnwelem 6916 ressuppss 6939 ressuppssdif 6941 smores 7076 smores3 7077 smores2 7078 tz7.44-2 7130 tz7.44-3 7131 frfnom 7157 sbthlem5 7691 sbthlem7 7693 domss2 7736 imafi 7872 ordtypelem4 8041 wdomima2g 8106 r0weon 8448 imadomg 8967 dmaddpi 9320 dmmulpi 9321 ltweuz 12182 dmhashres 12531 limsupgle 13547 fvsetsid 15160 setsres 15163 lubdm 16237 glbdm 16250 gsumzaddlem 17566 dprdcntz2 17683 lmres 20328 imacmp 20424 qtoptop2 20726 kqdisj 20759 metreslem 21389 setsmstopn 21505 ismbl 22492 mbfres 22612 dvres3a 22881 cpnres 22903 dvlipcn 22958 dvlip2 22959 c1lip3 22963 dvcnvrelem1 22981 dvcvx 22984 dvlog 23608 cusgrasizeindslem2 25214 eupares 25715 hlimcaui 26901 dfrdg2 30454 sltres 30563 nodense 30590 nofulllem5 30607 caures 32101 ssbnd 32132 mapfzcons1 35571 diophrw 35613 eldioph2lem1 35614 eldioph2lem2 35615 rp-imass 36378 fourierdlem93 38073 fouriersw 38105 eldmressn 38634 fnresfnco 38637 afvres 38684 uhgrspansubgrlem 39372 |
Copyright terms: Public domain | W3C validator |