Theorem nfres 5974

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

This proof depends on syntax axioms:  Ⅎwnfc 2907  Vcvv 3450   ∩ cin 3898   × cxp 5653   ↾ cres 5657

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-in 3906  df-opab 5168  df-xp 5661  df-res 5667

This theorem is used by:  nfima  6064  nffrecs  8282  frsucmpt  8427  frsucmptn  8428  nfoi  9486  prdsdsf  24593  prdsxmet  24595  limciun  26121  nosupbnd2  27952  noinfbnd2  27967  2ndresdju  33122  gsumpart  33503  bnj1446  35554  bnj1447  35555  bnj1448  35556  bnj1466  35562  bnj1467  35563  bnj1519  35574  bnj1520  35575  bnj1529  35579  feqresmptf  46060  limcperiod  46458  xlimconst2  46663  cncfiooicclem1  46721  stoweidlem28  46856  nfdfat  48015  setrec2lem2  50620  setrec2  50621