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

Theorem nfres 5854
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 5566 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 nfres.1 . . 3 𝑥𝐴
3 nfres.2 . . . 4 𝑥𝐵
4 nfcv 2982 . . . 4 𝑥V
53, 4nfxp 5587 . . 3 𝑥(𝐵 × V)
62, 5nfin 4197 . 2 𝑥(𝐴 ∩ (𝐵 × V))
71, 6nfcxfr 2980 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2966  Vcvv 3500  cin 3939   × cxp 5552  cres 5556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-in 3947  df-opab 5126  df-xp 5560  df-res 5566
This theorem is referenced by:  nfima  5935  nfwrecs  7940  frsucmpt  8064  frsucmptn  8065  nfoi  8967  prdsdsf  22892  prdsxmet  22894  limciun  24407  bnj1446  32201  bnj1447  32202  bnj1448  32203  bnj1466  32209  bnj1467  32210  bnj1519  32221  bnj1520  32222  bnj1529  32226  trpredlem1  32950  trpredrec  32961  nffrecs  33004  nosupbnd2  33100  feqresmptf  41364  limcperiod  41774  xlimconst2  41981  cncfiooicclem1  42041  stoweidlem28  42179  nfdfat  43192  setrec2lem2  44629  setrec2  44630
  Copyright terms: Public domain W3C validator