Theorem nfres 5940

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

Hypotheses

Ref	Expression
nfres.1	⊢ Ⅎ𝑥𝐴
nfres.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfres	⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Proof of Theorem nfres

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

Syntax hints:  Ⅎwnfc 2884  Vcvv 3430   ∩ cin 3889   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-v 3432  df-in 3897  df-opab 5149  df-xp 5630  df-res 5636

This theorem is referenced by:  nfima  6027  nffrecs  8226  frsucmpt  8370  frsucmptn  8371  nfoi  9422  prdsdsf  24342  prdsxmet  24344  limciun  25871  nosupbnd2  27694  noinfbnd2  27709  2ndresdju  32737  gsumpart  33139  bnj1446  35203  bnj1447  35204  bnj1448  35205  bnj1466  35211  bnj1467  35212  bnj1519  35223  bnj1520  35224  bnj1529  35228  feqresmptf  45678  limcperiod  46076  xlimconst2  46281  cncfiooicclem1  46339  stoweidlem28  46474  nfdfat  47587  setrec2lem2  50181  setrec2  50182