MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnresi Structured version   Unicode version

Theorem rnresi 5341
Description: The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
Assertion
Ref Expression
rnresi  |-  ran  (  _I  |`  A )  =  A

Proof of Theorem rnresi
StepHypRef Expression
1 df-ima 5005 . 2  |-  (  _I  " A )  =  ran  (  _I  |`  A )
2 imai 5340 . 2  |-  (  _I  " A )  =  A
31, 2eqtr3i 2491 1  |-  ran  (  _I  |`  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374    _I cid 4783   ran crn 4993    |` cres 4994   "cima 4995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005
This theorem is referenced by:  resiima  5342  iordsmo  7018  dfac9  8505  restid2  14675  sylow1lem2  16408  sylow3lem1  16436  lsslinds  18626  wilthlem3  23065  ausisusgra  24018  cusgraexi  24130  idssxp  27128  relexprn  28520  diophrw  30283  lnrfg  30661  dvsid  30791  fourierdlem60  31422  fourierdlem61  31423  usgresvm1  31837
  Copyright terms: Public domain W3C validator