Theorem nfres 5971

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 5662	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2922	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5683	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4121	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2920	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

This proof depends on syntax axioms:  Ⅎwnfc 2907  Vcvv 3450   ∩ cin 4089   × cxp 5648   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-in 4091  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  nfima  6063  nffrecs  8305  frsucmpt  8450  frsucmptn  8451  nfoi  9512  setrec2lem2  9980  setrec2  9981  prdsdsf  24692  prdsxmet  24694  limciun  26220  nosupbnd2  28079  noinfbnd2  28094  2ndresdju  33291  gsumpart  33671  bnj1446  35722  bnj1447  35723  bnj1448  35724  bnj1466  35730  bnj1467  35731  bnj1519  35742  bnj1520  35743  bnj1529  35747  srepdflem1  36005  srepdflem2  36006  feqresmptf  46337  limcperiod  46734  xlimconst2  46939  cncfiooicclem1  46997  stoweidlem28  47132  nfdfat  48291