# Metamath Proof Explorer

## 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{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfres.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfres ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({{A}↾}_{{B}}\right)$

### Proof

Step Hyp Ref Expression
1 nfres.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfres.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 df-res ${⊢}{{A}↾}_{{B}}={A}\cap \left({B}×\mathrm{V}\right)$
4 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{V}$
5 2 4 nfxp ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({B}×\mathrm{V}\right)$
6 1 5 nfin ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}\cap \left({B}×\mathrm{V}\right)\right)$
7 3 6 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({{A}↾}_{{B}}\right)$