Theorem nfres 5319

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 5050	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		nfres.1	. . 3 ⊢ Ⅎ𝑥𝐴
3		nfres.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4		nfcv 2751	. . . 4 ⊢ Ⅎ𝑥V
5	3, 4	nfxp 5066	. . 3 ⊢ Ⅎ𝑥(𝐵 × V)
6	2, 5	nfin 3782	. 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V))
7	1, 6	nfcxfr 2749	1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)

Syntax hints:  Ⅎwnfc 2738  Vcvv 3173   ∩ cin 3539   × cxp 5036   ↾ cres 5040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-opab 4644  df-xp 5044  df-res 5050

This theorem is referenced by:  nfima  5393  nfwrecs  7296  frsucmpt  7420  frsucmptn  7421  nfoi  8302  prdsdsf  21982  prdsxmet  21984  limciun  23464  bnj1446  30367  bnj1447  30368  bnj1448  30369  bnj1466  30375  bnj1467  30376  bnj1519  30387  bnj1520  30388  bnj1529  30392  trpredlem1  30971  trpredrec  30982  wessf1ornlem  38366  limcperiod  38695  cncfiooicclem1  38779  stoweidlem28  38921  nfdfat  39859  setrec2lem2  42240  setrec2  42241