Theorem rnresi 6073

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

This proof depends on syntax axioms:   = wceq 1570   I cid 5545  ran crn 5652   ↾ cres 5653   “ cima 5654

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  resiima  6074  f1oi  6861  iordsmo  8358  dfac9  10208  relexprng  15192  relexpfld  15195  restid2  17594  sylow1lem2  19806  sylow3lem1  19834  lsslinds  22130  wilthlem3  27390  ausgrusgrb  29739  umgrres1lem  29884  umgrres1  29888  nbupgrres  29938  cusgrexilem2  30016  cusgrsize  30028  cycpmconjslem2  33709  diophrw  43749  lnrfg  44105  rclexi  44600  cnvrcl0  44610  dfrtrcl5  44614  dfrcl2  44659  brfvrcld2  44677  iunrelexp0  44687  relexpiidm  44689  relexp01min  44698  dvsid  45300  fourierdlem60  47145  fourierdlem61  47146  stgredg  49023  gpgedg  49112  uspgrsprfo  49215  imaidfu  50187  idfudiag1lem  50600