Metamath Proof Explorer

Theorem fvilbd

Description: A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020)

Ref Expression
Hypothesis fvilbd.r 
|- ( ph -> R e. _V )
Assertion fvilbd 
|- ( ph -> R C_ ( _I ` R ) )

Proof

Step Hyp Ref Expression
1 fvilbd.r 
 |-  ( ph -> R e. _V )
2 ssid 
 |-  R C_ R
3 fvi 
 |-  ( R e. _V -> ( _I ` R ) = R )
4 1 3 syl 
 |-  ( ph -> ( _I ` R ) = R )
5 2 4 sseqtrrid 
 |-  ( ph -> R C_ ( _I ` R ) )