Theorem dmresi 6041

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 3960	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5897	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3985	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5999	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 232	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1560  Vcvv 3454   ⊆ wss 3904   I cid 5541  dom cdm 5647   ↾ cres 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5542  df-xp 5653  df-rel 5654  df-dm 5657  df-res 5659

This theorem is referenced by:  iordsmo  8328  residfi  9281  hartogslem1  9490  dfac9  10093  hsmexlem5  10387  relexpdmg  15055  relexpfld  15062  relexpaddg  15066  dirdm  18632  islinds2  21865  lindsind2  21871  f1linds  21877  wilthlem3  27134  ausgrusgrb  29366  usgrres1  29516  usgrexilem  29641  filnetlem3  36740  filnetlem4  36741  rclexi  44191  dfrtrcl5  44205  dfrcl2  44250  brfvrcld2  44268  iunrelexp0  44278  relexpiidm  44280  relexp01min  44289  ushggricedg  48549  stgrusgra  48581  gpgiedgdmel  48671  gpgusgra  48679  uspgrsprfo  48770