Theorem nfres 5968

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

Syntax hints:  Ⅎwnfc 2883  Vcvv 3459   ∩ cin 3925   × cxp 5652   ↾ cres 5656

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-v 3461  df-in 3933  df-opab 5182  df-xp 5660  df-res 5666

This theorem is referenced by:  nfima  6055  nffrecs  8282  nfwrecsOLD  8316  frsucmpt  8452  frsucmptn  8453  nfoi  9528  prdsdsf  24306  prdsxmet  24308  limciun  25847  nosupbnd2  27680  noinfbnd2  27695  2ndresdju  32627  gsumpart  33051  bnj1446  35076  bnj1447  35077  bnj1448  35078  bnj1466  35084  bnj1467  35085  bnj1519  35096  bnj1520  35097  bnj1529  35101  feqresmptf  45255  limcperiod  45657  xlimconst2  45864  cncfiooicclem1  45922  stoweidlem28  46057  nfdfat  47156  setrec2lem2  49558  setrec2  49559