Theorem nfres 5937

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 5633	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2895	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5654	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 4173	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2893	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2880  Vcvv 3437   ∩ cin 3897   × cxp 5619   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-v 3439  df-in 3905  df-opab 5158  df-xp 5627  df-res 5633

This theorem is referenced by:  nfima  6024  nffrecs  8222  frsucmpt  8366  frsucmptn  8367  nfoi  9411  prdsdsf  24302  prdsxmet  24304  limciun  25842  nosupbnd2  27675  noinfbnd2  27690  2ndresdju  32653  gsumpart  33074  bnj1446  35129  bnj1447  35130  bnj1448  35131  bnj1466  35137  bnj1467  35138  bnj1519  35149  bnj1520  35150  bnj1529  35154  feqresmptf  45391  limcperiod  45790  xlimconst2  45995  cncfiooicclem1  46053  stoweidlem28  46188  nfdfat  47289  setrec2lem2  49855  setrec2  49856