Theorem nfres 5933

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 5630	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2901	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5651	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4153	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2899	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2886  Vcvv 3431   ∩ cin 3882   × cxp 5616   ↾ cres 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-v 3433  df-in 3890  df-opab 5135  df-xp 5624  df-res 5630

This theorem is referenced by:  nfima  6020  nffrecs  8223  frsucmpt  8367  frsucmptn  8368  nfoi  9419  prdsdsf  24350  prdsxmet  24352  limciun  25879  nosupbnd2  27698  noinfbnd2  27713  2ndresdju  32741  gsumpart  33144  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1466  35235  bnj1467  35236  bnj1519  35247  bnj1520  35248  bnj1529  35252  feqresmptf  45675  limcperiod  46073  xlimconst2  46278  cncfiooicclem1  46336  stoweidlem28  46471  nfdfat  47590  setrec2lem2  50184  setrec2  50185