MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfres Structured version   Visualization version   GIF version

Theorem nfres 5999
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
StepHypRef Expression
1 df-res 5697 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 nfres.1 . . 3 𝑥𝐴
3 nfres.2 . . . 4 𝑥𝐵
4 nfcv 2905 . . . 4 𝑥V
53, 4nfxp 5718 . . 3 𝑥(𝐵 × V)
62, 5nfin 4224 . 2 𝑥(𝐴 ∩ (𝐵 × V))
71, 6nfcxfr 2903 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2890  Vcvv 3480  cin 3950   × cxp 5683  cres 5687
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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-v 3482  df-in 3958  df-opab 5206  df-xp 5691  df-res 5697
This theorem is referenced by:  nfima  6086  nffrecs  8308  nfwrecsOLD  8342  frsucmpt  8478  frsucmptn  8479  nfoi  9554  prdsdsf  24377  prdsxmet  24379  limciun  25929  nosupbnd2  27761  noinfbnd2  27776  2ndresdju  32659  gsumpart  33060  bnj1446  35059  bnj1447  35060  bnj1448  35061  bnj1466  35067  bnj1467  35068  bnj1519  35079  bnj1520  35080  bnj1529  35084  feqresmptf  45236  limcperiod  45643  xlimconst2  45850  cncfiooicclem1  45908  stoweidlem28  46043  nfdfat  47139  setrec2lem2  49213  setrec2  49214
  Copyright terms: Public domain W3C validator