Theorem rnresi 6027

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 5631	. 2 ⊢ ( I “ 𝐴) = ran ( I ↾ 𝐴)
2		imai 6026	. 2 ⊢ ( I “ 𝐴) = 𝐴
3	1, 2	eqtr3i 2764	1 ⊢ ran ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1547   I cid 5512  ran crn 5619   ↾ cres 5620   “ cima 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631

This theorem is referenced by:  resiima  6028  f1oi  6805  iordsmo  8287  dfac9  10050  relexprng  14999  relexpfld  15002  restid2  17384  sylow1lem2  19565  sylow3lem1  19593  lsslinds  21806  wilthlem3  27051  ausgrusgrb  29252  umgrres1lem  29397  umgrres1  29401  nbupgrres  29451  cusgrexilem2  29529  cusgrsize  29541  cycpmconjslem2  33236  diophrw  43208  lnrfg  43564  rclexi  44059  cnvrcl0  44069  dfrtrcl5  44073  dfrcl2  44118  brfvrcld2  44136  iunrelexp0  44146  relexpiidm  44148  relexp01min  44157  dvsid  44775  fourierdlem60  46609  fourierdlem61  46610  stgredg  48447  gpgedg  48536  uspgrsprfo  48639  imaidfu  49600  idfudiag1lem  50013