Metamath Proof Explorer

Theorem bj-funidres

Description: The restricted identity relation is a function. (Contributed by BJ, 27-Dec-2023)

TODO: relabel funi to funid.

Ref Expression
Assertion bj-funidres 
|- Fun ( _I |` V )

Proof

Step Hyp Ref Expression
1 funi 
 |-  Fun _I
2 funres 
 |-  ( Fun _I -> Fun ( _I |` V ) )
3 1 2 ax-mp 
 |-  Fun ( _I |` V )