Theorem nfres 5818

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

Syntax hints:  Ⅎwnfc 2897  Vcvv 3407   ∩ cin 3853   × cxp 5515   ↾ cres 5519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-rab 3077  df-in 3861  df-opab 5088  df-xp 5523  df-res 5529

This theorem is referenced by:  nfima  5902  nfwrecs  7952  frsucmpt  8076  frsucmptn  8077  nfoi  8996  prdsdsf  23054  prdsxmet  23056  limciun  24578  2ndresdju  30494  gsumpart  30826  bnj1446  32530  bnj1447  32531  bnj1448  32532  bnj1466  32538  bnj1467  32539  bnj1519  32550  bnj1520  32551  bnj1529  32555  trpredlem1  33298  trpredrec  33309  nffrecs  33366  nosupbnd2  33469  noinfbnd2  33484  feqresmptf  42218  limcperiod  42621  xlimconst2  42828  cncfiooicclem1  42886  stoweidlem28  43021  nfdfat  44036  setrec2lem2  45574  setrec2  45575