Metamath Proof Explorer

Theorem fvi

Description: The value of the identity function. (Contributed by NM, 1-May-2004) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fvi 
|- ( A e. V -> ( _I ` A ) = A )

Proof

Step Hyp Ref Expression
1 funi 
 |-  Fun _I
2 ididg 
 |-  ( A e. V -> A _I A )
3 funbrfv 
 |-  ( Fun _I -> ( A _I A -> ( _I ` A ) = A ) )
4 1 2 3 mpsyl 
 |-  ( A e. V -> ( _I ` A ) = A )