![]() |
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 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 ↾ 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |