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	|- F/_ x A
	nfres.2	|- F/_ x B
Assertion	nfres	|- F/_ x ( A |` B )

Proof

Step	Hyp	Ref	Expression
1		nfres.1	|- F/_ x A
2		nfres.2	|- F/_ x B
3		df-res	|- ( A |` B ) = ( A i^i ( B X. _V ) )
4		nfcv	|- F/_ x _V
5	2 4	nfxp	|- F/_ x ( B X. _V )
6	1 5	nfin	|- F/_ x ( A i^i ( B X. _V ) )
7	3 6	nfcxfr	|- F/_ x ( A |` B )