Theorem nfres 5825

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

Syntax hints:  Ⅎwnfc 2899  Vcvv 3409   ∩ cin 3857   × cxp 5522   ↾ cres 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-in 3865  df-opab 5095  df-xp 5530  df-res 5536

This theorem is referenced by:  nfima  5909  nfwrecs  7959  frsucmpt  8083  frsucmptn  8084  nfoi  9011  prdsdsf  23069  prdsxmet  23071  limciun  24593  2ndresdju  30509  gsumpart  30841  bnj1446  32545  bnj1447  32546  bnj1448  32547  bnj1466  32553  bnj1467  32554  bnj1519  32565  bnj1520  32566  bnj1529  32570  trpredlem1  33313  trpredrec  33324  nffrecs  33381  nosupbnd2  33484  noinfbnd2  33499  feqresmptf  42233  limcperiod  42636  xlimconst2  42843  cncfiooicclem1  42901  stoweidlem28  43036  nfdfat  44051  setrec2lem2  45615  setrec2  45616