Metamath Proof Explorer

Theorem ressid

Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypothesis ressid.1 
|- B = ( Base ` W )
Assertion ressid 
|- ( W e. X -> ( W |`s B ) = W )

Proof

Step Hyp Ref Expression
1 ressid.1 
 |-  B = ( Base ` W )
2 ssid 
 |-  B C_ B
3 1 fvexi 
 |-  B e. _V
4 eqid 
 |-  ( W |`s B ) = ( W |`s B )
5 4 1 ressid2 
 |-  ( ( B C_ B /\ W e. X /\ B e. _V ) -> ( W |`s B ) = W )
6 2 3 5 mp3an13 
 |-  ( W e. X -> ( W |`s B ) = W )