MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmresi Structured version   Visualization version   GIF version

Theorem dmresi 5897
Description: The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
Assertion
Ref Expression
dmresi dom ( I ↾ 𝐴) = 𝐴

Proof of Theorem dmresi
StepHypRef Expression
1 ssv 3970 . . 3 𝐴 ⊆ V
2 dmi 5767 . . 3 dom I = V
31, 2sseqtrri 3983 . 2 𝐴 ⊆ dom I
4 ssdmres 5852 . 2 (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴)
53, 4mpbi 232 1 dom ( I ↾ 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  Vcvv 3473  wss 3913   I cid 5435  dom cdm 5531  cres 5533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043  df-opab 5105  df-id 5436  df-xp 5537  df-rel 5538  df-dm 5541  df-res 5543
This theorem is referenced by:  fnresiOLD  6453  iordsmo  7972  residfi  8783  hartogslem1  8984  dfac9  9540  hsmexlem5  9830  relexpdmg  14381  relexpfld  14388  relexpaddg  14392  dirdm  17823  islinds2  20933  lindsind2  20939  f1linds  20945  wilthlem3  25634  ausgrusgrb  26937  usgrres1  27084  usgrexilem  27209  filnetlem3  33736  filnetlem4  33737  rclexi  40110  cnvrcl0  40120  dfrtrcl5  40124  dfrcl2  40154  brfvrcld2  40172  iunrelexp0  40182  relexpiidm  40184  relexp01min  40193  ushrisomgr  44151  uspgrsprfo  44168
  Copyright terms: Public domain W3C validator