Theorem dmresi 6009

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 3956	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5868	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3981	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5970	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 230	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1541  Vcvv 3438   ⊆ wss 3899   I cid 5516  dom cdm 5622   ↾ cres 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-id 5517  df-xp 5628  df-rel 5629  df-dm 5632  df-res 5634

This theorem is referenced by:  iordsmo  8287  residfi  9236  hartogslem1  9445  dfac9  10045  hsmexlem5  10338  relexpdmg  14963  relexpfld  14970  relexpaddg  14974  dirdm  18521  islinds2  21766  lindsind2  21772  f1linds  21778  wilthlem3  27034  ausgrusgrb  29187  usgrres1  29337  usgrexilem  29462  filnetlem3  36523  filnetlem4  36524  rclexi  43798  dfrtrcl5  43812  dfrcl2  43857  brfvrcld2  43875  iunrelexp0  43885  relexpiidm  43887  relexp01min  43896  ushggricedg  48115  stgrusgra  48147  gpgiedgdmel  48237  gpgusgra  48245  uspgrsprfo  48336