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		starvid	$$⊢{\ast }_{𝑟}=\mathrm{Slot}{\mathrm{*}}_{\mathrm{ndx}}$$
4		starvndxnbasendx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
5	1 2 3 4	resseqnbas	$$⊢A\in V\to \underset{\dot{}}{\ast }={\mathrm{*}}_S$$