Theorem ressstarv

Description: *r is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015)

	Ref	Expression
Hypotheses	ressmulr.1	|- S = ( R |`s A )
	ressstarv.2	|- .* = ( *r ` R )
Assertion	ressstarv	|- ( A e. V -> .* = ( *r ` S ) )

Proof

Step	Hyp	Ref	Expression
1		ressmulr.1	|- S = ( R |`s A )
2		ressstarv.2	|- .* = ( *r ` R )
3		starvid	|- *r = Slot ( *r ` ndx )
4		starvndxnbasendx	|- ( *r ` ndx ) =/= ( Base ` ndx )
5	1 2 3 4	resseqnbas	|- ( A e. V -> .* = ( *r ` S ) )