Theorem ressunif

Description: UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017)

	Ref	Expression
Hypotheses	ressunif.1	$$⊢H=G{\upharpoonright }_{𝑠}A$$
	ressunif.2	$$⊢U=\mathrm{UnifSet}\left(G\right)$$
Assertion	ressunif	$$⊢A\in V\to U=\mathrm{UnifSet}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		ressunif.1	$$⊢H=G{\upharpoonright }_{𝑠}A$$
2		ressunif.2	$$⊢U=\mathrm{UnifSet}\left(G\right)$$
3		unifid	$$⊢\mathrm{UnifSet}=\mathrm{Slot}\mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
4		unifndxnbasendx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
5	1 2 3 4	resseqnbas	$$⊢A\in V\to U=\mathrm{UnifSet}\left(H\right)$$