Theorem dmresi 6011

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

Syntax hints:   = wceq 1541  Vcvv 3440   ⊆ wss 3901   I cid 5518  dom cdm 5624   ↾ cres 5626

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-dm 5634  df-res 5636

This theorem is referenced by:  iordsmo  8289  residfi  9240  hartogslem1  9449  dfac9  10049  hsmexlem5  10342  relexpdmg  14967  relexpfld  14974  relexpaddg  14978  dirdm  18525  islinds2  21770  lindsind2  21776  f1linds  21782  wilthlem3  27038  ausgrusgrb  29240  usgrres1  29390  usgrexilem  29515  filnetlem3  36576  filnetlem4  36577  rclexi  43877  dfrtrcl5  43891  dfrcl2  43936  brfvrcld2  43954  iunrelexp0  43964  relexpiidm  43966  relexp01min  43975  ushggricedg  48194  stgrusgra  48226  gpgiedgdmel  48316  gpgusgra  48324  uspgrsprfo  48415