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

Theorem nfres 5848
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 5560 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 nfres.1 . . 3 𝑥𝐴
3 nfres.2 . . . 4 𝑥𝐵
4 nfcv 2974 . . . 4 𝑥V
53, 4nfxp 5581 . . 3 𝑥(𝐵 × V)
62, 5nfin 4190 . 2 𝑥(𝐴 ∩ (𝐵 × V))
71, 6nfcxfr 2972 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2958  Vcvv 3492  cin 3932   × cxp 5546  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-in 3940  df-opab 5120  df-xp 5554  df-res 5560
This theorem is referenced by:  nfima  5930  nfwrecs  7938  frsucmpt  8062  frsucmptn  8063  nfoi  8966  prdsdsf  22904  prdsxmet  22906  limciun  24419  bnj1446  32214  bnj1447  32215  bnj1448  32216  bnj1466  32222  bnj1467  32223  bnj1519  32234  bnj1520  32235  bnj1529  32239  trpredlem1  32963  trpredrec  32974  nffrecs  33017  nosupbnd2  33113  feqresmptf  41375  limcperiod  41785  xlimconst2  41992  cncfiooicclem1  42052  stoweidlem28  42190  nfdfat  43203  setrec2lem2  44725  setrec2  44726
  Copyright terms: Public domain W3C validator