Theorem dmresi 6039

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 3983	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5901	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 4008	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 6000	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 230	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3459   ⊆ wss 3926   I cid 5547  dom cdm 5654   ↾ cres 5656

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-dm 5664  df-res 5666

This theorem is referenced by:  iordsmo  8371  residfi  9350  hartogslem1  9556  dfac9  10151  hsmexlem5  10444  relexpdmg  15061  relexpfld  15068  relexpaddg  15072  dirdm  18610  islinds2  21773  lindsind2  21779  f1linds  21785  wilthlem3  27032  ausgrusgrb  29144  usgrres1  29294  usgrexilem  29419  filnetlem3  36398  filnetlem4  36399  rclexi  43639  dfrtrcl5  43653  dfrcl2  43698  brfvrcld2  43716  iunrelexp0  43726  relexpiidm  43728  relexp01min  43737  ushggricedg  47940  stgrusgra  47971  gpgiedgdmel  48053  gpgusgra  48061  uspgrsprfo  48123