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

Theorem dmresi 5179
Description: The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
Assertion
Ref Expression
dmresi  |-  dom  (  _I  |`  A )  =  A

Proof of Theorem dmresi
StepHypRef Expression
1 ssv 3484 . . 3  |-  A  C_  _V
2 dmi 5068 . . 3  |-  dom  _I  =  _V
31, 2sseqtr4i 3497 . 2  |-  A  C_  dom  _I
4 ssdmres 5145 . 2  |-  ( A 
C_  dom  _I  <->  dom  (  _I  |`  A )  =  A )
53, 4mpbi 211 1  |-  dom  (  _I  |`  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   _Vcvv 3080    C_ wss 3436    _I cid 4763   dom cdm 4853    |` cres 4855
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-dm 4863  df-res 4865
This theorem is referenced by:  fnresi  5711  iordsmo  7087  hartogslem1  8066  dfac9  8573  hsmexlem5  8867  relexpdmg  13105  relexpfld  13112  relexpaddg  13116  dirdm  16479  islinds2  19369  lindsind2  19375  f1linds  19381  wilthlem3  23993  ausisusgra  25080  cusgraexilem2  25193  idssxp  28229  filnetlem3  31041  filnetlem4  31042  rclexi  36192  rtrclex  36194  rtrclexi  36198  cnvrcl0  36202  dfrtrcl5  36206  dfrcl2  36236  brfvrcld2  36254  iunrelexp0  36264  relexpiidm  36266  relexp01min  36275  idhe  36353  residfi  38893  ausgrusgrb  39046  umgrres1  39148  usgrres1  39149  usgrexi  39262  usgresvm1  39374  usgresvm1ALT  39378
  Copyright terms: Public domain W3C validator