Metamath Proof Explorer

Theorem resiexd

Description: The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020)

Ref Expression
Hypothesis resiexd.b φ B V
Assertion resiexd φ I B V


Step Hyp Ref Expression
1 resiexd.b φ B V
2 funi Fun I
3 resfunexg Fun I B V I B V
4 2 1 3 sylancr φ I B V