![]() |
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 5646 | . 2 ⊢ ( I “ 𝐴) = ran ( I ↾ 𝐴) | |
2 | imai 6026 | . 2 ⊢ ( I “ 𝐴) = 𝐴 | |
3 | 1, 2 | eqtr3i 2766 | 1 ⊢ ran ( I ↾ 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 I cid 5530 ran crn 5634 ↾ cres 5635 “ cima 5636 |
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 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
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 2714 df-cleq 2728 df-clel 2814 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-br 5106 df-opab 5168 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 |
This theorem is referenced by: resiima 6028 iordsmo 8302 dfac9 10071 relexprng 14930 relexpfld 14933 restid2 17311 sylow1lem2 19379 sylow3lem1 19407 lsslinds 21235 wilthlem3 26417 ausgrusgrb 28063 umgrres1lem 28205 umgrres1 28209 nbupgrres 28259 cusgrexilem2 28337 cusgrsize 28349 cycpmconjslem2 31948 diophrw 41059 lnrfg 41423 rclexi 41868 cnvrcl0 41878 dfrtrcl5 41882 dfrcl2 41927 brfvrcld2 41945 iunrelexp0 41955 relexpiidm 41957 relexp01min 41966 dvsid 42592 fourierdlem60 44378 fourierdlem61 44379 uspgrsprfo 46021 |
Copyright terms: Public domain | W3C validator |