Theorem dmresi 6003

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 5864	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3985	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5964	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 230	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3436   ⊆ wss 3903   I cid 5513  dom cdm 5619   ↾ cres 5621

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 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-dm 5629  df-res 5631

This theorem is referenced by:  iordsmo  8280  residfi  9228  hartogslem1  9434  dfac9  10031  hsmexlem5  10324  relexpdmg  14949  relexpfld  14956  relexpaddg  14960  dirdm  18506  islinds2  21720  lindsind2  21726  f1linds  21732  wilthlem3  26978  ausgrusgrb  29110  usgrres1  29260  usgrexilem  29385  filnetlem3  36364  filnetlem4  36365  rclexi  43598  dfrtrcl5  43612  dfrcl2  43657  brfvrcld2  43675  iunrelexp0  43685  relexpiidm  43687  relexp01min  43696  ushggricedg  47921  stgrusgra  47953  gpgiedgdmel  48043  gpgusgra  48051  uspgrsprfo  48142