Theorem dmresi 6050

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 3988	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5912	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 4013	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 6011	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 230	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1539  Vcvv 3463   ⊆ wss 3931   I cid 5557  dom cdm 5665   ↾ cres 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-opab 5186  df-id 5558  df-xp 5671  df-rel 5672  df-dm 5675  df-res 5677

This theorem is referenced by:  iordsmo  8379  residfi  9360  hartogslem1  9564  dfac9  10159  hsmexlem5  10452  relexpdmg  15063  relexpfld  15070  relexpaddg  15074  dirdm  18614  islinds2  21787  lindsind2  21793  f1linds  21799  wilthlem3  27049  ausgrusgrb  29110  usgrres1  29260  usgrexilem  29385  filnetlem3  36340  filnetlem4  36341  rclexi  43590  dfrtrcl5  43604  dfrcl2  43649  brfvrcld2  43667  iunrelexp0  43677  relexpiidm  43679  relexp01min  43688  ushggricedg  47854  stgrusgra  47884  gpgusgra  47970  uspgrsprfo  48022