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 
|- ( ph -> B e. V )
Assertion resiexd 
|- ( ph -> ( _I |` B ) e. _V )

Proof

Step Hyp Ref Expression
1 resiexd.b 
 |-  ( ph -> B e. V )
2 funi 
 |-  Fun _I
3 resfunexg 
 |-  ( ( Fun _I /\ B e. V ) -> ( _I |` B ) e. _V )
4 2 1 3 sylancr 
 |-  ( ph -> ( _I |` B ) e. _V )