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		df-starv	|- *r = Slot 4
4		4nn	|- 4 e. NN
5		1lt4	|- 1 < 4
6	1 2 3 4 5	resslem	|- ( A e. V -> .* = ( *r ` S ) )