Theorem nfres 5820

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 5531	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2955	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5552	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4143	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2953	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2936  Vcvv 3441   ∩ cin 3880   × cxp 5517   ↾ cres 5521

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-in 3888  df-opab 5093  df-xp 5525  df-res 5531

This theorem is referenced by:  nfima  5904  nfwrecs  7932  frsucmpt  8056  frsucmptn  8057  nfoi  8962  prdsdsf  22974  prdsxmet  22976  limciun  24497  2ndresdju  30411  gsumpart  30740  bnj1446  32427  bnj1447  32428  bnj1448  32429  bnj1466  32435  bnj1467  32436  bnj1519  32447  bnj1520  32448  bnj1529  32452  trpredlem1  33179  trpredrec  33190  nffrecs  33233  nosupbnd2  33329  feqresmptf  41865  limcperiod  42270  xlimconst2  42477  cncfiooicclem1  42535  stoweidlem28  42670  nfdfat  43683  setrec2lem2  45224  setrec2  45225