Theorem nfres 5936

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 5635	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2891	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5656	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4177	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2876  Vcvv 3438   ∩ cin 3904   × cxp 5621   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3440  df-in 3912  df-opab 5158  df-xp 5629  df-res 5635

This theorem is referenced by:  nfima  6023  nffrecs  8223  frsucmpt  8367  frsucmptn  8368  nfoi  9425  prdsdsf  24271  prdsxmet  24273  limciun  25811  nosupbnd2  27644  noinfbnd2  27659  2ndresdju  32606  gsumpart  33023  bnj1446  35014  bnj1447  35015  bnj1448  35016  bnj1466  35022  bnj1467  35023  bnj1519  35034  bnj1520  35035  bnj1529  35039  feqresmptf  45212  limcperiod  45613  xlimconst2  45820  cncfiooicclem1  45878  stoweidlem28  46013  nfdfat  47115  setrec2lem2  49683  setrec2  49684