Theorem nfres 5982

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

This proof depends on syntax axioms:  Ⅎwnfc 2912  Vcvv 3457   ∩ cin 3905   × cxp 5661   ↾ cres 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-in 3913  df-opab 5176  df-xp 5669  df-res 5675

This theorem is used by:  nfima  6072  nffrecs  8282  frsucmpt  8427  frsucmptn  8428  nfoi  9479  prdsdsf  24555  prdsxmet  24557  limciun  26084  nosupbnd2  27911  noinfbnd2  27926  2ndresdju  33041  gsumpart  33423  bnj1446  35474  bnj1447  35475  bnj1448  35476  bnj1466  35482  bnj1467  35483  bnj1519  35494  bnj1520  35495  bnj1529  35499  feqresmptf  45979  limcperiod  46377  xlimconst2  46582  cncfiooicclem1  46640  stoweidlem28  46775  nfdfat  47897  setrec2lem2  50505  setrec2  50506