Theorem dmresi 6026

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 3974	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5888	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3999	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5987	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 230	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3450   ⊆ wss 3917   I cid 5535  dom cdm 5641   ↾ cres 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-dm 5651  df-res 5653

This theorem is referenced by:  iordsmo  8329  residfi  9296  hartogslem1  9502  dfac9  10097  hsmexlem5  10390  relexpdmg  15015  relexpfld  15022  relexpaddg  15026  dirdm  18566  islinds2  21729  lindsind2  21735  f1linds  21741  wilthlem3  26987  ausgrusgrb  29099  usgrres1  29249  usgrexilem  29374  filnetlem3  36375  filnetlem4  36376  rclexi  43611  dfrtrcl5  43625  dfrcl2  43670  brfvrcld2  43688  iunrelexp0  43698  relexpiidm  43700  relexp01min  43709  ushggricedg  47931  stgrusgra  47962  gpgiedgdmel  48044  gpgusgra  48052  uspgrsprfo  48140