Metamath Proof Explorer

Theorem fnresi

Description: The restricted identity relation is a function on the restricting class. (Contributed by NM, 27-Aug-2004) (Proof shortened by BJ, 27-Dec-2023)

Ref Expression
Assertion fnresi I A Fn A


Step Hyp Ref Expression
1 idfn I Fn V
2 ssv A V
3 fnssres I Fn V A V I A Fn A
4 1 2 3 mp2an I A Fn A