Theorem nfres 5988

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 5670	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2926	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5691	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4124	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2924	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

This proof depends on syntax axioms:  Ⅎwnfc 2911  Vcvv 3454   ∩ cin 4092   × cxp 5656   ↾ cres 5660

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-v 3456  df-in 4094  df-opab 5174  df-xp 5664  df-res 5670

This theorem is used by:  nfima  6082  nffrecs  8339  frsucmpt  8484  frsucmptn  8485  nfoi  9545  setrec2lem2  10013  setrec2  10014  prdsdsf  24741  prdsxmet  24743  limciun  26269  nosupbnd2  28130  noinfbnd2  28145  2ndresdju  33341  gsumpart  33723  bnj1446  35786  bnj1447  35787  bnj1448  35788  bnj1466  35794  bnj1467  35795  bnj1519  35806  bnj1520  35807  bnj1529  35811  srepdflem1  36126  srepdflem2  36127  feqresmptf  46516  limcperiod  46913  xlimconst2  47118  cncfiooicclem1  47176  stoweidlem28  47311  nfdfat  48470