Metamath Proof Explorer


Theorem ressvsca

Description: .s is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses resssca.1
|- H = ( G |`s A )
ressvsca.2
|- .x. = ( .s ` G )
Assertion ressvsca
|- ( A e. V -> .x. = ( .s ` H ) )

Proof

Step Hyp Ref Expression
1 resssca.1
 |-  H = ( G |`s A )
2 ressvsca.2
 |-  .x. = ( .s ` G )
3 vscaid
 |-  .s = Slot ( .s ` ndx )
4 vscandxnbasendx
 |-  ( .s ` ndx ) =/= ( Base ` ndx )
5 1 2 3 4 resseqnbas
 |-  ( A e. V -> .x. = ( .s ` H ) )