![]() |
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 5651 | . 2 ⊢ ( I “ 𝐴) = ran ( I ↾ 𝐴) | |
2 | imai 6031 | . 2 ⊢ ( I “ 𝐴) = 𝐴 | |
3 | 1, 2 | eqtr3i 2761 | 1 ⊢ ran ( I ↾ 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 I cid 5535 ran crn 5639 ↾ cres 5640 “ cima 5641 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3406 df-v 3448 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-br 5111 df-opab 5173 df-id 5536 df-xp 5644 df-rel 5645 df-cnv 5646 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 |
This theorem is referenced by: resiima 6033 iordsmo 8308 dfac9 10081 relexprng 14943 relexpfld 14946 restid2 17326 sylow1lem2 19395 sylow3lem1 19423 lsslinds 21274 wilthlem3 26456 ausgrusgrb 28179 umgrres1lem 28321 umgrres1 28325 nbupgrres 28375 cusgrexilem2 28453 cusgrsize 28465 cycpmconjslem2 32074 diophrw 41140 lnrfg 41504 rclexi 42009 cnvrcl0 42019 dfrtrcl5 42023 dfrcl2 42068 brfvrcld2 42086 iunrelexp0 42096 relexpiidm 42098 relexp01min 42107 dvsid 42733 fourierdlem60 44527 fourierdlem61 44528 uspgrsprfo 46170 |
Copyright terms: Public domain | W3C validator |