![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnresi | Structured version Visualization version GIF version |
Description: The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.) |
Ref | Expression |
---|---|
rnresi | ⊢ ran ( I ↾ 𝐴) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ima 5231 | . 2 ⊢ ( I “ 𝐴) = ran ( I ↾ 𝐴) | |
2 | imai 5588 | . 2 ⊢ ( I “ 𝐴) = 𝐴 | |
3 | 1, 2 | eqtr3i 2748 | 1 ⊢ ran ( I ↾ 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1596 I cid 5127 ran crn 5219 ↾ cres 5220 “ cima 5221 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pr 5011 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ral 3019 df-rex 3020 df-rab 3023 df-v 3306 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-sn 4286 df-pr 4288 df-op 4292 df-br 4761 df-opab 4821 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 |
This theorem is referenced by: resiima 5590 idssxp 6122 iordsmo 7574 dfac9 9071 relexprng 13906 relexpfld 13909 restid2 16214 sylow1lem2 18135 sylow3lem1 18163 lsslinds 20293 wilthlem3 24916 ausgrusgrb 26180 umgrres1lem 26322 umgrres1 26326 nbupgrres 26385 cusgrexilem2 26469 cusgrsize 26481 diophrw 37741 lnrfg 38108 rclexi 38341 rtrclex 38343 rtrclexi 38347 cnvrcl0 38351 dfrtrcl5 38355 dfrcl2 38385 brfvrcld2 38403 iunrelexp0 38413 relexpiidm 38415 relexp01min 38424 idhe 38500 dvsid 38949 fourierdlem60 40803 fourierdlem61 40804 uspgrsprfo 42183 |
Copyright terms: Public domain | W3C validator |