Theorem dmresi 5715

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 3844	. . 3 ⊢ 𝐴 ⊆ V
2		dmi 5587	. . 3 ⊢ dom I = V
3	1, 2	sseqtr4i 3857	. 2 ⊢ 𝐴 ⊆ dom I
4		ssdmres 5671	. 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
5	3, 4	mpbi 222	1 ⊢ dom ( I ↾ 𝐴) = 𝐴

Syntax hints:   = wceq 1601  Vcvv 3398   ⊆ wss 3792   I cid 5262  dom cdm 5357   ↾ cres 5359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889  df-opab 4951  df-id 5263  df-xp 5363  df-rel 5364  df-dm 5367  df-res 5369

This theorem is referenced by:  fnresi  6256  idssxpOLD  6257  iordsmo  7739  residfi  8537  hartogslem1  8738  dfac9  9295  hsmexlem5  9589  relexpdmg  14193  relexpfld  14200  relexpaddg  14204  dirdm  17624  islinds2  20560  lindsind2  20566  f1linds  20572  wilthlem3  25252  ausgrusgrb  26518  umgrres1  26665  usgrres1  26666  usgrexilem  26792  filnetlem3  32967  filnetlem4  32968  rclexi  38889  rtrclex  38891  rtrclexi  38895  cnvrcl0  38899  dfrtrcl5  38903  dfrcl2  38933  brfvrcld2  38951  iunrelexp0  38961  relexpiidm  38963  relexp01min  38972  idhe  39047  ushrisomgr  42764  uspgrsprfo  42781