![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmresi | Structured version Visualization version GIF version |
Description: The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.) |
Ref | Expression |
---|---|
dmresi | ⊢ dom ( I ↾ 𝐴) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssv 4004 | . . 3 ⊢ 𝐴 ⊆ V | |
2 | dmi 5926 | . . 3 ⊢ dom I = V | |
3 | 1, 2 | sseqtrri 4017 | . 2 ⊢ 𝐴 ⊆ dom I |
4 | ssdmres 6020 | . 2 ⊢ (𝐴 ⊆ dom I ↔ dom ( I ↾ 𝐴) = 𝐴) | |
5 | 3, 4 | mpbi 229 | 1 ⊢ dom ( I ↾ 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 Vcvv 3471 ⊆ wss 3947 I cid 5577 dom cdm 5680 ↾ cres 5682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5151 df-opab 5213 df-id 5578 df-xp 5686 df-rel 5687 df-dm 5690 df-res 5692 |
This theorem is referenced by: iordsmo 8382 residfi 9363 hartogslem1 9571 dfac9 10165 hsmexlem5 10459 relexpdmg 15027 relexpfld 15034 relexpaddg 15038 dirdm 18597 islinds2 21752 lindsind2 21758 f1linds 21764 wilthlem3 27020 ausgrusgrb 28996 usgrres1 29146 usgrexilem 29271 filnetlem3 35869 filnetlem4 35870 rclexi 43048 dfrtrcl5 43062 dfrcl2 43107 brfvrcld2 43125 iunrelexp0 43135 relexpiidm 43137 relexp01min 43146 ushggricedg 47244 uspgrsprfo 47261 |
Copyright terms: Public domain | W3C validator |