Theorem dmresi 6055

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 3969	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5912	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3994	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 6013	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 233	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1567  Vcvv 3463   ⊆ wss 3913   I cid 5556  dom cdm 5662   ↾ cres 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-id 5557  df-xp 5668  df-rel 5669  df-dm 5672  df-res 5674

This theorem is referenced by:  iordsmo  8344  residfi  9295  hartogslem1  9504  dfac9  10120  hsmexlem5  10414  relexpdmg  15079  relexpfld  15086  relexpaddg  15090  dirdm  18656  islinds2  21932  lindsind2  21938  f1linds  21944  wilthlem3  27200  ausgrusgrb  29456  usgrres1  29606  usgrexilem  29731  filnetlem3  36780  filnetlem4  36781  rclexi  44233  dfrtrcl5  44247  dfrcl2  44292  brfvrcld2  44310  iunrelexp0  44320  relexpiidm  44322  relexp01min  44331  ushggricedg  48581  stgrusgra  48613  gpgiedgdmel  48703  gpgusgra  48711  uspgrsprfo  48802