Theorem dmresi 6054

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 3961	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5911	. . 3 ⊢ dom I = V
3	1, 2	sseqtrri 3986	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 6012	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 233	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1570  Vcvv 3455   ⊆ wss 3905   I cid 5555  dom cdm 5661   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-dm 5671  df-res 5673

This theorem is referenced by:  iordsmo  8340  residfi  9291  hartogslem1  9500  dfac9  10116  hsmexlem5  10409  relexpdmg  15075  relexpfld  15082  relexpaddg  15086  dirdm  18651  islinds2  21963  lindsind2  21969  f1linds  21975  wilthlem3  27234  ausgrusgrb  29515  usgrres1  29665  usgrexilem  29790  filnetlem3  36911  filnetlem4  36912  rclexi  44361  dfrtrcl5  44375  dfrcl2  44420  brfvrcld2  44438  iunrelexp0  44448  relexpiidm  44450  relexp01min  44459  ushggricedg  48712  stgrusgra  48744  gpgiedgdmel  48834  gpgusgra  48842  uspgrsprfo  48933