Theorem dmresi 6056

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 3962	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5913	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3987	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 6014	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 233	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3457   ⊆ wss 3906   I cid 5557  dom cdm 5663   ↾ cres 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-dm 5673  df-res 5675

This theorem is used by:  iordsmo  8350  residfi  9302  hartogslem1  9511  dfac9  10136  hsmexlem5  10429  relexpdmg  15105  relexpfld  15112  relexpaddg  15116  dirdm  18680  islinds2  22015  lindsind2  22021  f1linds  22027  wilthlem3  27287  ausgrusgrb  29575  usgrres1  29725  usgrexilem  29850  filnetlem3  36950  filnetlem4  36951  rclexi  44401  dfrtrcl5  44415  dfrcl2  44460  brfvrcld2  44478  iunrelexp0  44488  relexpiidm  44490  relexp01min  44499  ushggricedg  48752  stgrusgra  48784  gpgiedgdmel  48874  gpgusgra  48882  uspgrsprfo  48973