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	⊢ Ⅎ 𝑥 𝐴
	nfres.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfres	⊢ Ⅎ 𝑥 ( 𝐴 ↾ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfres.1	⊢ Ⅎ 𝑥 𝐴
2		nfres.2	⊢ Ⅎ 𝑥 𝐵
3		df-res	⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
4		nfcv	⊢ Ⅎ 𝑥 V
5	2 4	nfxp	⊢ Ⅎ 𝑥 ( 𝐵 × V )
6	1 5	nfin	⊢ Ⅎ 𝑥 ( 𝐴 ∩ ( 𝐵 × V ) )
7	3 6	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐴 ↾ 𝐵 )