Theorem dmresi 6004

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 3939	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5863	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3964	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5965	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 231	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1547  Vcvv 3431   ⊆ wss 3883   I cid 5512  dom cdm 5618   ↾ cres 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-dm 5628  df-res 5630

This theorem is referenced by:  iordsmo  8287  residfi  9238  hartogslem1  9447  dfac9  10050  hsmexlem5  10343  relexpdmg  14995  relexpfld  15002  relexpaddg  15006  dirdm  18557  islinds2  21788  lindsind2  21794  f1linds  21800  wilthlem3  27051  ausgrusgrb  29252  usgrres1  29402  usgrexilem  29527  filnetlem3  36608  filnetlem4  36609  rclexi  44059  dfrtrcl5  44073  dfrcl2  44118  brfvrcld2  44136  iunrelexp0  44146  relexpiidm  44148  relexp01min  44157  ushggricedg  48418  stgrusgra  48450  gpgiedgdmel  48540  gpgusgra  48548  uspgrsprfo  48639