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

Theorem rnresi 5914
Description: The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
Assertion
Ref Expression
rnresi ran ( I ↾ 𝐴) = 𝐴

Proof of Theorem rnresi
StepHypRef Expression
1 df-ima 5536 . 2 ( I “ 𝐴) = ran ( I ↾ 𝐴)
2 imai 5913 . 2 ( I “ 𝐴) = 𝐴
31, 2eqtr3i 2826 1 ran ( I ↾ 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538   I cid 5427  ran crn 5524  cres 5525  cima 5526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536
This theorem is referenced by:  resiima  5915  iordsmo  7981  dfac9  9551  relexprng  14401  relexpfld  14404  restid2  16700  sylow1lem2  18720  sylow3lem1  18748  lsslinds  20524  wilthlem3  25659  ausgrusgrb  26962  umgrres1lem  27104  umgrres1  27108  nbupgrres  27158  cusgrexilem2  27236  cusgrsize  27248  cycpmconjslem2  30851  diophrw  39697  lnrfg  40060  rclexi  40312  cnvrcl0  40322  dfrtrcl5  40326  dfrcl2  40372  brfvrcld2  40390  iunrelexp0  40400  relexpiidm  40402  relexp01min  40411  dvsid  41032  fourierdlem60  42805  fourierdlem61  42806  uspgrsprfo  44373
  Copyright terms: Public domain W3C validator