Metamath Proof Explorer

Theorem dmresi

Description: The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004)

Ref Expression
Assertion dmresi 
|- dom ( _I |` A ) = A

Proof

Step Hyp Ref Expression
1 ssv 
 |-  A C_ _V
2 dmi 
 |-  dom _I = _V
3 1 2 sseqtrri 
 |-  A C_ dom _I
4 ssdmres 
 |-  ( A C_ dom _I <-> dom ( _I |` A ) = A )
5 3 4 mpbi 
 |-  dom ( _I |` A ) = A