Theorem nfres 5946

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 5643	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2898	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5664	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4164	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2896	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2883  Vcvv 3429   ∩ cin 3888   × cxp 5629   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-v 3431  df-in 3896  df-opab 5148  df-xp 5637  df-res 5643

This theorem is referenced by:  nfima  6033  nffrecs  8233  frsucmpt  8377  frsucmptn  8378  nfoi  9429  prdsdsf  24332  prdsxmet  24334  limciun  25861  nosupbnd2  27680  noinfbnd2  27695  2ndresdju  32722  gsumpart  33124  bnj1446  35187  bnj1447  35188  bnj1448  35189  bnj1466  35195  bnj1467  35196  bnj1519  35207  bnj1520  35208  bnj1529  35212  feqresmptf  45660  limcperiod  46058  xlimconst2  46263  cncfiooicclem1  46321  stoweidlem28  46456  nfdfat  47575  setrec2lem2  50169  setrec2  50170