Theorem nfres 5952

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 5650	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2891	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5671	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4187	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2876  Vcvv 3447   ∩ cin 3913   × cxp 5636   ↾ cres 5640

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3449  df-in 3921  df-opab 5170  df-xp 5644  df-res 5650

This theorem is referenced by:  nfima  6039  nffrecs  8262  frsucmpt  8406  frsucmptn  8407  nfoi  9467  prdsdsf  24255  prdsxmet  24257  limciun  25795  nosupbnd2  27628  noinfbnd2  27643  2ndresdju  32573  gsumpart  32997  bnj1446  35035  bnj1447  35036  bnj1448  35037  bnj1466  35043  bnj1467  35044  bnj1519  35055  bnj1520  35056  bnj1529  35060  feqresmptf  45225  limcperiod  45626  xlimconst2  45833  cncfiooicclem1  45891  stoweidlem28  46026  nfdfat  47128  setrec2lem2  49683  setrec2  49684