Theorem rnresi 6079

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

This proof depends on syntax axioms:   = wceq 1570   I cid 5557  ran crn 5664   ↾ cres 5665   “ cima 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  resiima  6080  f1oi  6863  iordsmo  8350  dfac9  10136  relexprng  15107  relexpfld  15110  restid2  17505  sylow1lem2  19713  sylow3lem1  19741  lsslinds  22031  wilthlem3  27285  ausgrusgrb  29573  umgrres1lem  29718  umgrres1  29722  nbupgrres  29772  cusgrexilem2  29850  cusgrsize  29862  cycpmconjslem2  33539  diophrw  43548  lnrfg  43904  rclexi  44399  cnvrcl0  44409  dfrtrcl5  44413  dfrcl2  44458  brfvrcld2  44476  iunrelexp0  44486  relexpiidm  44488  relexp01min  44497  dvsid  45099  fourierdlem60  46938  fourierdlem61  46939  stgredg  48779  gpgedg  48868  uspgrsprfo  48971  imaidfu  49945  idfudiag1lem  50358