Theorem dmresi 6019

Description: The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)

Assertion

Ref	Expression
dmresi	⊢ dom ( I ↾ 𝐴) = 𝐴

Proof of Theorem dmresi

Step	Hyp	Ref	Expression
1		ssv 3960	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5878	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3985	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5980	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 230	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1542  Vcvv 3442   ⊆ wss 3903   I cid 5526  dom cdm 5632   ↾ cres 5634

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-dm 5642  df-res 5644

This theorem is referenced by:  iordsmo  8299  residfi  9250  hartogslem1  9459  dfac9  10059  hsmexlem5  10352  relexpdmg  14977  relexpfld  14984  relexpaddg  14988  dirdm  18535  islinds2  21783  lindsind2  21789  f1linds  21795  wilthlem3  27051  ausgrusgrb  29254  usgrres1  29404  usgrexilem  29529  filnetlem3  36600  filnetlem4  36601  rclexi  43975  dfrtrcl5  43989  dfrcl2  44034  brfvrcld2  44052  iunrelexp0  44062  relexpiidm  44064  relexp01min  44073  ushggricedg  48291  stgrusgra  48323  gpgiedgdmel  48413  gpgusgra  48421  uspgrsprfo  48512