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

Theorem nfres 5567
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 5289 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 nfres.1 . . 3 𝑥𝐴
3 nfres.2 . . . 4 𝑥𝐵
4 nfcv 2907 . . . 4 𝑥V
53, 4nfxp 5310 . . 3 𝑥(𝐵 × V)
62, 5nfin 3980 . 2 𝑥(𝐴 ∩ (𝐵 × V))
71, 6nfcxfr 2905 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2894  Vcvv 3350  cin 3731   × cxp 5275  cres 5279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-in 3739  df-opab 4872  df-xp 5283  df-res 5289
This theorem is referenced by:  nfima  5656  nfwrecs  7612  frsucmpt  7737  frsucmptn  7738  nfoi  8626  prdsdsf  22451  prdsxmet  22453  limciun  23949  bnj1446  31561  bnj1447  31562  bnj1448  31563  bnj1466  31569  bnj1467  31570  bnj1519  31581  bnj1520  31582  bnj1529  31586  trpredlem1  32170  trpredrec  32181  nffrecs  32222  nosupbnd2  32306  wessf1ornlem  40018  feqresmptf  40075  limcperiod  40498  xlimconst2  40699  cncfiooicclem1  40744  stoweidlem28  40882  nfdfat  41875  setrec2lem2  43110  setrec2  43111
  Copyright terms: Public domain W3C validator