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

Theorem nfres 5825
 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 5536 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 nfres.1 . . 3 𝑥𝐴
3 nfres.2 . . . 4 𝑥𝐵
4 nfcv 2919 . . . 4 𝑥V
53, 4nfxp 5557 . . 3 𝑥(𝐵 × V)
62, 5nfin 4121 . 2 𝑥(𝐴 ∩ (𝐵 × V))
71, 6nfcxfr 2917 1 𝑥(𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2899  Vcvv 3409   ∩ cin 3857   × cxp 5522   ↾ cres 5526 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-in 3865  df-opab 5095  df-xp 5530  df-res 5536 This theorem is referenced by:  nfima  5909  nfwrecs  7959  frsucmpt  8083  frsucmptn  8084  nfoi  9011  prdsdsf  23069  prdsxmet  23071  limciun  24593  2ndresdju  30509  gsumpart  30841  bnj1446  32545  bnj1447  32546  bnj1448  32547  bnj1466  32553  bnj1467  32554  bnj1519  32565  bnj1520  32566  bnj1529  32570  trpredlem1  33313  trpredrec  33324  nffrecs  33381  nosupbnd2  33484  noinfbnd2  33499  feqresmptf  42233  limcperiod  42636  xlimconst2  42843  cncfiooicclem1  42901  stoweidlem28  43036  nfdfat  44051  setrec2lem2  45615  setrec2  45616
 Copyright terms: Public domain W3C validator