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

Theorem nfres 5275
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 5011 . 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 2629 . . . 4  |-  F/_ x _V
53, 4nfxp 5026 . . 3  |-  F/_ x
( B  X.  _V )
62, 5nfin 3705 . 2  |-  F/_ x
( A  i^i  ( B  X.  _V ) )
71, 6nfcxfr 2627 1  |-  F/_ x
( A  |`  B )
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2615   _Vcvv 3113    i^i cin 3475    X. cxp 4997    |` cres 5001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-in 3483  df-opab 4506  df-xp 5005  df-res 5011
This theorem is referenced by:  nfima  5345  frsucmpt  7104  frsucmptn  7105  nfoi  7940  prdsdsf  20697  prdsxmet  20699  limciun  22125  trpredlem1  29163  trpredrec  29174  nfwrecs  29191  limcperiod  31397  cncfiooicclem1  31459  stoweidlem28  31555  nfdfat  31909  bnj1446  33397  bnj1447  33398  bnj1448  33399  bnj1466  33405  bnj1467  33406  bnj1519  33417  bnj1520  33418  bnj1529  33422
  Copyright terms: Public domain W3C validator