Theorem nfres 5978

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 5671	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2931	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5692	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4185	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2929	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2916  Vcvv 3463   ∩ cin 3912   × cxp 5657   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-v 3465  df-in 3920  df-opab 5175  df-xp 5665  df-res 5671

This theorem is referenced by:  nfima  6068  nffrecs  8276  frsucmpt  8421  frsucmptn  8422  nfoi  9472  prdsdsf  24489  prdsxmet  24491  limciun  26018  nosupbnd2  27842  noinfbnd2  27857  2ndresdju  32931  gsumpart  33320  bnj1446  35374  bnj1447  35375  bnj1448  35376  bnj1466  35382  bnj1467  35383  bnj1519  35394  bnj1520  35395  bnj1529  35399  feqresmptf  45831  limcperiod  46229  xlimconst2  46434  cncfiooicclem1  46492  stoweidlem28  46627  nfdfat  47746  setrec2lem2  50350  setrec2  50351