Theorem nfres 5963

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 5655	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2923	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5676	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4174	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2921	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2908  Vcvv 3453   ∩ cin 3901   × cxp 5641   ↾ cres 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3455  df-in 3909  df-opab 5160  df-xp 5649  df-res 5655

This theorem is referenced by:  nfima  6053  nffrecs  8258  frsucmpt  8403  frsucmptn  8404  nfoi  9456  prdsdsf  24415  prdsxmet  24417  limciun  25944  nosupbnd2  27768  noinfbnd2  27783  2ndresdju  32812  gsumpart  33204  bnj1446  35301  bnj1447  35302  bnj1448  35303  bnj1466  35309  bnj1467  35310  bnj1519  35321  bnj1520  35322  bnj1529  35326  feqresmptf  45767  limcperiod  46165  xlimconst2  46370  cncfiooicclem1  46428  stoweidlem28  46563  nfdfat  47682  setrec2lem2  50276  setrec2  50277