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

Theorem nfres 5396
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 5124 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 nfres.1 . . 3 𝑥𝐴
3 nfres.2 . . . 4 𝑥𝐵
4 nfcv 2763 . . . 4 𝑥V
53, 4nfxp 5140 . . 3 𝑥(𝐵 × V)
62, 5nfin 3818 . 2 𝑥(𝐴 ∩ (𝐵 × V))
71, 6nfcxfr 2761 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2750  Vcvv 3198  cin 3571   × cxp 5110  cres 5114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-in 3579  df-opab 4711  df-xp 5118  df-res 5124
This theorem is referenced by:  nfima  5472  nfwrecs  7406  frsucmpt  7530  frsucmptn  7531  nfoi  8416  prdsdsf  22166  prdsxmet  22168  limciun  23652  bnj1446  31098  bnj1447  31099  bnj1448  31100  bnj1466  31106  bnj1467  31107  bnj1519  31118  bnj1520  31119  bnj1529  31123  trpredlem1  31711  trpredrec  31722  nosupbnd2  31846  wessf1ornlem  39193  feqresmptf  39255  limcperiod  39666  cncfiooicclem1  39875  stoweidlem28  40014  nfdfat  40979  setrec2lem2  42212  setrec2  42213
  Copyright terms: Public domain W3C validator