Theorem nfres

Description: Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypotheses	nfres.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfres.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfres	$$⊢\underset{\_}{Ⅎ}x\left({A\upharpoonright }_B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfres.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfres.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-res	$$⊢{A\upharpoonright }_B=A\cap \left(B\times \mathrm{V}\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
5	2 4	nfxp	$$⊢\underset{\_}{Ⅎ}x\left(B\times \mathrm{V}\right)$$
6	1 5	nfin	$$⊢\underset{\_}{Ⅎ}x\left(A\cap \left(B\times \mathrm{V}\right)\right)$$
7	3 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left({A\upharpoonright }_B\right)$$