Theorem nfres 5972

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 5663	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2923	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5684	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4170	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2921	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

This proof depends on syntax axioms:  Ⅎwnfc 2908  Vcvv 3451   ∩ cin 3898   × cxp 5649   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3453  df-in 3906  df-opab 5168  df-xp 5657  df-res 5663

This theorem is used by:  nfima  6064  nffrecs  8294  frsucmpt  8439  frsucmptn  8440  nfoi  9501  setrec2lem2  9969  setrec2  9970  prdsdsf  24679  prdsxmet  24681  limciun  26207  nosupbnd2  28066  noinfbnd2  28081  2ndresdju  33236  gsumpart  33617  bnj1446  35668  bnj1447  35669  bnj1448  35670  bnj1466  35676  bnj1467  35677  bnj1519  35688  bnj1520  35689  bnj1529  35693  feqresmptf  46212  limcperiod  46609  xlimconst2  46814  cncfiooicclem1  46872  stoweidlem28  47007  nfdfat  48166