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

Theorem nfres 5319
 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 5050 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 nfres.1 . . 3 𝑥𝐴
3 nfres.2 . . . 4 𝑥𝐵
4 nfcv 2751 . . . 4 𝑥V
53, 4nfxp 5066 . . 3 𝑥(𝐵 × V)
62, 5nfin 3782 . 2 𝑥(𝐴 ∩ (𝐵 × V))
71, 6nfcxfr 2749 1 𝑥(𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2738  Vcvv 3173   ∩ cin 3539   × cxp 5036   ↾ cres 5040 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-opab 4644  df-xp 5044  df-res 5050 This theorem is referenced by:  nfima  5393  nfwrecs  7296  frsucmpt  7420  frsucmptn  7421  nfoi  8302  prdsdsf  21982  prdsxmet  21984  limciun  23464  bnj1446  30367  bnj1447  30368  bnj1448  30369  bnj1466  30375  bnj1467  30376  bnj1519  30387  bnj1520  30388  bnj1529  30392  trpredlem1  30971  trpredrec  30982  wessf1ornlem  38366  limcperiod  38695  cncfiooicclem1  38779  stoweidlem28  38921  nfdfat  39859  setrec2lem2  42240  setrec2  42241
 Copyright terms: Public domain W3C validator