Theorem rnresi 6035

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

Syntax hints:   = wceq 1540   I cid 5525  ran crn 5632   ↾ cres 5633   “ cima 5634

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  resiima  6036  iordsmo  8303  dfac9  10066  relexprng  14988  relexpfld  14991  restid2  17369  sylow1lem2  19505  sylow3lem1  19533  lsslinds  21716  wilthlem3  26956  ausgrusgrb  29068  umgrres1lem  29213  umgrres1  29217  nbupgrres  29267  cusgrexilem2  29345  cusgrsize  29358  cycpmconjslem2  33085  diophrw  42720  lnrfg  43081  rclexi  43577  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  brfvrcld2  43654  iunrelexp0  43664  relexpiidm  43666  relexp01min  43675  dvsid  44293  fourierdlem60  46137  fourierdlem61  46138  stgredg  47928  gpgedg  48009  uspgrsprfo  48109  imaidfu  49072  idfudiag1lem  49485