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

Theorem rnresi 5200
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 4866 . 2  |-  (  _I  " A )  =  ran  (  _I  |`  A )
2 imai 5199 . 2  |-  (  _I  " A )  =  A
31, 2eqtr3i 2453 1  |-  ran  (  _I  |`  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    _I cid 4763   ran crn 4854    |` cres 4855   "cima 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866
This theorem is referenced by:  resiima  5201  iordsmo  7087  dfac9  8573  relexprng  13109  relexpfld  13112  restid2  15328  sylow1lem2  17250  sylow3lem1  17278  lsslinds  19387  wilthlem3  23993  ausisusgra  25080  cusgraexi  25194  idssxp  28229  diophrw  35570  lnrfg  35948  rclexi  36192  rtrclex  36194  rtrclexi  36198  cnvrcl0  36202  dfrtrcl5  36206  dfrcl2  36236  brfvrcld2  36254  iunrelexp0  36264  relexpiidm  36266  relexp01min  36275  idhe  36353  dvsid  36650  fourierdlem60  37970  fourierdlem61  37971  ausgrusgrb  39046  usgrres1  39149  nbumgrres  39202  cusgrexi  39263  cusgrsize  39271  usgresvm1  39374  usgresvm1ALT  39378
  Copyright terms: Public domain W3C validator