Theorem rnresi 6072

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

This proof depends on syntax axioms:   = wceq 1569   I cid 5544  ran crn 5651   ↾ cres 5652   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  resiima  6073  f1oi  6863  iordsmo  8366  dfac9  10216  relexprng  15200  relexpfld  15203  restid2  17602  sylow1lem2  19814  sylow3lem1  19842  lsslinds  22138  wilthlem3  27398  ausgrusgrb  29747  umgrres1lem  29892  umgrres1  29896  nbupgrres  29946  cusgrexilem2  30024  cusgrsize  30036  cycpmconjslem2  33759  diophrw  43814  lnrfg  44165  rclexi  44659  cnvrcl0  44669  dfrtrcl5  44673  dfrcl2  44718  brfvrcld2  44736  iunrelexp0  44746  relexpiidm  44748  relexp01min  44757  dvsid  45359  fourierdlem60  47220  fourierdlem61  47221  stgredg  49098  gpgedg  49187  uspgrsprfo  49290  imaidfu  50262  idfudiag1lem  50675