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

Theorem nfres 4957
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  |-  F/_ x A
nfres.2  |-  F/_ x B
Assertion
Ref Expression
nfres  |-  F/_ x
( A  |`  B )

Proof of Theorem nfres
StepHypRef Expression
1 df-res 4701 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 nfres.1 . . 3  |-  F/_ x A
3 nfres.2 . . . 4  |-  F/_ x B
4 nfcv 2419 . . . 4  |-  F/_ x _V
53, 4nfxp 4715 . . 3  |-  F/_ x
( B  X.  _V )
62, 5nfin 3375 . 2  |-  F/_ x
( A  i^i  ( B  X.  _V ) )
71, 6nfcxfr 2416 1  |-  F/_ x
( A  |`  B )
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2406   _Vcvv 2788    i^i cin 3151    X. cxp 4687    |` cres 4691
This theorem is referenced by:  nfima  5020  frsucmpt  6450  frsucmptn  6451  nfoi  7229  axdclem  8146  prdsdsf  17931  prdsxmet  17933  limciun  19244  trpredlem1  24230  trpredrec  24241  stoweidlem28  27777  nfdfat  27993  bnj1446  29075  bnj1447  29076  bnj1448  29077  bnj1466  29083  bnj1467  29084  bnj1519  29095  bnj1520  29096  bnj1529  29100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-in 3159  df-opab 4078  df-xp 4695  df-res 4701
  Copyright terms: Public domain W3C validator