Theorem rnresi 5625

Description: The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)

Assertion

Ref	Expression
rnresi	⊢ ran ( I ↾ 𝐴) = 𝐴

Proof of Theorem rnresi

Step	Hyp	Ref	Expression
1		df-ima 5267	. 2 ⊢ ( I “ 𝐴) = ran ( I ↾ 𝐴)
2		imai 5624	. 2 ⊢ ( I “ 𝐴) = 𝐴
3	1, 2	eqtr3i 2772	1 ⊢ ran ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1620   I cid 5161  ran crn 5255   ↾ cres 5256   “ cima 5257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-br 4793  df-opab 4853  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267

This theorem is referenced by:  resiima  5626  idssxp  6158  iordsmo  7611  dfac9  9121  relexprng  13956  relexpfld  13959  restid2  16264  sylow1lem2  18185  sylow3lem1  18213  lsslinds  20343  wilthlem3  24966  ausgrusgrb  26230  umgrres1lem  26372  umgrres1  26376  nbupgrres  26435  cusgrexilem2  26519  cusgrsize  26531  diophrw  37793  lnrfg  38160  rclexi  38393  rtrclex  38395  rtrclexi  38399  cnvrcl0  38403  dfrtrcl5  38407  dfrcl2  38437  brfvrcld2  38455  iunrelexp0  38465  relexpiidm  38467  relexp01min  38476  idhe  38552  dvsid  39001  fourierdlem60  40855  fourierdlem61  40856  uspgrsprfo  42235