Theorem nfres 5941

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 5643	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2891	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5664	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4183	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2876  Vcvv 3444   ∩ cin 3910   × cxp 5629   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3446  df-in 3918  df-opab 5165  df-xp 5637  df-res 5643

This theorem is referenced by:  nfima  6028  nffrecs  8239  frsucmpt  8383  frsucmptn  8384  nfoi  9443  prdsdsf  24231  prdsxmet  24233  limciun  25771  nosupbnd2  27604  noinfbnd2  27619  2ndresdju  32546  gsumpart  32970  bnj1446  35008  bnj1447  35009  bnj1448  35010  bnj1466  35016  bnj1467  35017  bnj1519  35028  bnj1520  35029  bnj1529  35033  feqresmptf  45198  limcperiod  45599  xlimconst2  45806  cncfiooicclem1  45864  stoweidlem28  45999  nfdfat  47101  setrec2lem2  49656  setrec2  49657