Theorem dmresi 5599

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 3775	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5479	. . 3 ⊢ dom I = V
3	1, 2	sseqtr4i 3788	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5562	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 220	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1631  Vcvv 3351   ⊆ wss 3724   I cid 5157  dom cdm 5250   ↾ cres 5252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4788  df-opab 4848  df-id 5158  df-xp 5256  df-rel 5257  df-dm 5260  df-res 5262

This theorem is referenced by:  fnresi  6149  idssxp  6150  iordsmo  7608  residfi  8404  hartogslem1  8604  dfac9  9161  hsmexlem5  9455  relexpdmg  13991  relexpfld  13998  relexpaddg  14002  dirdm  17443  islinds2  20370  lindsind2  20376  f1linds  20382  wilthlem3  25018  ausgrusgrb  26283  umgrres1  26430  usgrres1  26431  usgrexilem  26572  filnetlem3  32713  filnetlem4  32714  rclexi  38449  rtrclex  38451  rtrclexi  38455  cnvrcl0  38459  dfrtrcl5  38463  dfrcl2  38493  brfvrcld2  38511  iunrelexp0  38521  relexpiidm  38523  relexp01min  38532  idhe  38608  uspgrsprfo  42285