Theorem dmresi 5607

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 3758	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5487	. . 3 ⊢ dom I = V
3	1, 2	sseqtr4i 3771	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5570	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 220	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1624  Vcvv 3332   ⊆ wss 3707   I cid 5165  dom cdm 5258   ↾ cres 5260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797  df-opab 4857  df-id 5166  df-xp 5264  df-rel 5265  df-dm 5268  df-res 5270

This theorem is referenced by:  fnresi  6161  idssxp  6162  iordsmo  7615  residfi  8404  hartogslem1  8604  dfac9  9142  hsmexlem5  9436  relexpdmg  13973  relexpfld  13980  relexpaddg  13984  dirdm  17427  islinds2  20346  lindsind2  20352  f1linds  20358  wilthlem3  24987  ausgrusgrb  26251  umgrres1  26397  usgrres1  26398  usgrexilem  26538  filnetlem3  32673  filnetlem4  32674  rclexi  38416  rtrclex  38418  rtrclexi  38422  cnvrcl0  38426  dfrtrcl5  38430  dfrcl2  38460  brfvrcld2  38478  iunrelexp0  38488  relexpiidm  38490  relexp01min  38499  idhe  38575  uspgrsprfo  42258