Theorem nfres 5999

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 5697	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2905	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5718	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4224	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2903	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2890  Vcvv 3480   ∩ cin 3950   × cxp 5683   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-v 3482  df-in 3958  df-opab 5206  df-xp 5691  df-res 5697

This theorem is referenced by:  nfima  6086  nffrecs  8308  nfwrecsOLD  8342  frsucmpt  8478  frsucmptn  8479  nfoi  9554  prdsdsf  24377  prdsxmet  24379  limciun  25929  nosupbnd2  27761  noinfbnd2  27776  2ndresdju  32659  gsumpart  33060  bnj1446  35059  bnj1447  35060  bnj1448  35061  bnj1466  35067  bnj1467  35068  bnj1519  35079  bnj1520  35080  bnj1529  35084  feqresmptf  45236  limcperiod  45643  xlimconst2  45850  cncfiooicclem1  45908  stoweidlem28  46043  nfdfat  47139  setrec2lem2  49213  setrec2  49214