Theorem dmresi 6081

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 4033	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5946	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 4046	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 6042	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 230	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1537  Vcvv 3488   ⊆ wss 3976   I cid 5592  dom cdm 5700   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-dm 5710  df-res 5712

This theorem is referenced by:  iordsmo  8413  residfi  9406  hartogslem1  9611  dfac9  10206  hsmexlem5  10499  relexpdmg  15091  relexpfld  15098  relexpaddg  15102  dirdm  18670  islinds2  21856  lindsind2  21862  f1linds  21868  wilthlem3  27131  ausgrusgrb  29200  usgrres1  29350  usgrexilem  29475  filnetlem3  36346  filnetlem4  36347  rclexi  43577  dfrtrcl5  43591  dfrcl2  43636  brfvrcld2  43654  iunrelexp0  43664  relexpiidm  43666  relexp01min  43675  ushggricedg  47780  uspgrsprfo  47871