Theorem rnresi 6060

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

Syntax hints:   = wceq 1559   I cid 5537  ran crn 5644   ↾ cres 5645   “ cima 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656

This theorem is referenced by:  resiima  6061  f1oi  6840  iordsmo  8322  dfac9  10087  relexprng  15053  relexpfld  15056  restid2  17450  sylow1lem2  19630  sylow3lem1  19658  lsslinds  21871  wilthlem3  27122  ausgrusgrb  29323  umgrres1lem  29468  umgrres1  29472  nbupgrres  29522  cusgrexilem2  29600  cusgrsize  29612  cycpmconjslem2  33296  diophrw  43301  lnrfg  43657  rclexi  44152  cnvrcl0  44162  dfrtrcl5  44166  dfrcl2  44211  brfvrcld2  44229  iunrelexp0  44239  relexpiidm  44241  relexp01min  44250  dvsid  44868  fourierdlem60  46701  fourierdlem61  46702  stgredg  48539  gpgedg  48628  uspgrsprfo  48731  imaidfu  49692  idfudiag1lem  50105