Theorem ressstarv

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

	Ref	Expression
Hypotheses	ressmulr.1	$$⊢S=R{\upharpoonright }_{𝑠}A$$
	ressstarv.2	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
Assertion	ressstarv	$$⊢A\in V\to \underset{\dot{}}{\ast }={\mathrm{*}}_S$$

Proof

Step	Hyp	Ref	Expression
1		ressmulr.1	$$⊢S=R{\upharpoonright }_{𝑠}A$$
2		ressstarv.2	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
3		df-starv	$$⊢{\ast }_{𝑟}=\mathrm{Slot}4$$
4		4nn	$$⊢4\in \mathbb{N}$$
5		1lt4	$$⊢1<4$$
6	1 2 3 4 5	resslem	$$⊢A\in V\to \underset{\dot{}}{\ast }={\mathrm{*}}_S$$