Theorem nfres 5944

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 5650	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2902	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5671	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4181	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2900	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2882  Vcvv 3446   ∩ cin 3912   × cxp 5636   ↾ cres 5640

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rab 3406  df-in 3920  df-opab 5173  df-xp 5644  df-res 5650

This theorem is referenced by:  nfima  6026  nffrecs  8219  nfwrecsOLD  8253  frsucmpt  8389  frsucmptn  8390  nfoi  9459  prdsdsf  23757  prdsxmet  23759  limciun  25295  nosupbnd2  27101  noinfbnd2  27116  2ndresdju  31632  gsumpart  31967  bnj1446  33746  bnj1447  33747  bnj1448  33748  bnj1466  33754  bnj1467  33755  bnj1519  33766  bnj1520  33767  bnj1529  33771  feqresmptf  43575  limcperiod  43989  xlimconst2  44196  cncfiooicclem1  44254  stoweidlem28  44389  nfdfat  45479  setrec2lem2  47259  setrec2  47260