Metamath Proof Explorer

Theorem rnresi

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

Ref Expression
Assertion rnresi 
|- ran ( _I |` A ) = A

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( _I " A ) = ran ( _I |` A )
2 imai 
 |-  ( _I " A ) = A
3 1 2 eqtr3i 
 |-  ran ( _I |` A ) = A