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

Theorem nfres 5264
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 5000 . 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 2616 . . . 4  |-  F/_ x _V
53, 4nfxp 5015 . . 3  |-  F/_ x
( B  X.  _V )
62, 5nfin 3691 . 2  |-  F/_ x
( A  i^i  ( B  X.  _V ) )
71, 6nfcxfr 2614 1  |-  F/_ x
( A  |`  B )
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2602   _Vcvv 3106    i^i cin 3460    X. cxp 4986    |` cres 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-in 3468  df-opab 4498  df-xp 4994  df-res 5000
This theorem is referenced by:  nfima  5333  frsucmpt  7095  frsucmptn  7096  nfoi  7931  prdsdsf  21036  prdsxmet  21038  limciun  22464  trpredlem1  29550  trpredrec  29561  nfwrecs  29578  limcperiod  31873  cncfiooicclem1  31935  stoweidlem28  32049  nfdfat  32454  bnj1446  34502  bnj1447  34503  bnj1448  34504  bnj1466  34510  bnj1467  34511  bnj1519  34522  bnj1520  34523  bnj1529  34527
  Copyright terms: Public domain W3C validator