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 2898	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5657	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4176	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2896	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2883  Vcvv 3440   ∩ cin 3900   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-v 3442  df-in 3908  df-opab 5161  df-xp 5630  df-res 5636

This theorem is referenced by:  nfima  6027  nffrecs  8225  frsucmpt  8369  frsucmptn  8370  nfoi  9419  prdsdsf  24311  prdsxmet  24313  limciun  25851  nosupbnd2  27684  noinfbnd2  27699  2ndresdju  32727  gsumpart  33146  bnj1446  35201  bnj1447  35202  bnj1448  35203  bnj1466  35209  bnj1467  35210  bnj1519  35221  bnj1520  35222  bnj1529  35226  feqresmptf  45475  limcperiod  45874  xlimconst2  46079  cncfiooicclem1  46137  stoweidlem28  46272  nfdfat  47373  setrec2lem2  49939  setrec2  49940