Theorem nfres 5882

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 5592	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2906	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5613	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4147	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2904	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2886  Vcvv 3422   ∩ cin 3882   × cxp 5578   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072  df-in 3890  df-opab 5133  df-xp 5586  df-res 5592

This theorem is referenced by:  nfima  5966  nffrecs  8070  nfwrecsOLD  8104  frsucmpt  8239  frsucmptn  8240  nfoi  9203  trpredlem1  9405  trpredrec  9415  prdsdsf  23428  prdsxmet  23430  limciun  24963  2ndresdju  30887  gsumpart  31217  bnj1446  32925  bnj1447  32926  bnj1448  32927  bnj1466  32933  bnj1467  32934  bnj1519  32945  bnj1520  32946  bnj1529  32950  nosupbnd2  33846  noinfbnd2  33861  feqresmptf  42661  limcperiod  43059  xlimconst2  43266  cncfiooicclem1  43324  stoweidlem28  43459  nfdfat  44506  setrec2lem2  46286  setrec2  46287