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

Syntax hints:  Ⅎwnfc 2910  Vcvv 3455   ∩ cin 3905   × cxp 5661   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-v 3457  df-in 3913  df-opab 5175  df-xp 5669  df-res 5675

This theorem is referenced by:  nfima  6072  nffrecs  8281  frsucmpt  8426  frsucmptn  8427  nfoi  9477  prdsdsf  24505  prdsxmet  24507  limciun  26034  nosupbnd2  27861  noinfbnd2  27876  2ndresdju  32975  gsumpart  33364  bnj1446  35414  bnj1447  35415  bnj1448  35416  bnj1466  35422  bnj1467  35423  bnj1519  35434  bnj1520  35435  bnj1529  35439  feqresmptf  45929  limcperiod  46327  xlimconst2  46532  cncfiooicclem1  46590  stoweidlem28  46725  nfdfat  47847  setrec2lem2  50455  setrec2  50456