Theorem rnresi 6030

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

Syntax hints:   = wceq 1540   I cid 5517  ran crn 5624   ↾ cres 5625   “ cima 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  resiima  6031  iordsmo  8287  dfac9  10050  relexprng  14972  relexpfld  14975  restid2  17353  sylow1lem2  19497  sylow3lem1  19525  lsslinds  21757  wilthlem3  26997  ausgrusgrb  29129  umgrres1lem  29274  umgrres1  29278  nbupgrres  29328  cusgrexilem2  29406  cusgrsize  29419  cycpmconjslem2  33116  diophrw  42752  lnrfg  43112  rclexi  43608  cnvrcl0  43618  dfrtrcl5  43622  dfrcl2  43667  brfvrcld2  43685  iunrelexp0  43695  relexpiidm  43697  relexp01min  43706  dvsid  44324  fourierdlem60  46167  fourierdlem61  46168  stgredg  47960  gpgedg  48049  uspgrsprfo  48152  imaidfu  49115  idfudiag1lem  49528