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

Theorem nffv 5873
Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypotheses
Ref Expression
nffv.1  |-  F/_ x F
nffv.2  |-  F/_ x A
Assertion
Ref Expression
nffv  |-  F/_ x
( F `  A
)

Proof of Theorem nffv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-fv 5596 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2629 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4491 . . 3  |-  F/ x  A F y
65nfiota 5555 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2627 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2615   class class class wbr 4447   iotacio 5549   ` cfv 5588
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-3an 975  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-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596
This theorem is referenced by:  nffvmpt1  5874  nffvd  5875  dffn5f  5922  fvmptss  5958  fvmptex  5960  fvmptf  5966  fvmptnf  5967  eqfnfv2f  5979  ralrnmpt  6030  ffnfvf  6048  funiunfvf  6149  dff13f  6155  nfiso  6208  nfrecs  7044  nfrdg  7080  rdgsucmptf  7094  rdgsucmptnf  7095  frsucmpt  7103  frsucmptn  7104  rankidb  8218  rankval4  8285  dfac8clem  8413  cardaleph  8470  hsmexlem2  8807  axcc2  8817  uniimadomf  8920  nfseq  12085  seqof2  12133  rlim2  13282  nfsum1  13475  nfsum  13476  sumeq2ii  13478  fsumrelem  13584  o1fsum  13590  prdsbas3  14736  prdsdsval2  14739  yonedalem4b  15403  gsum2d2lem  16804  coe1fzgsumdlem  18142  evl1gsumdlem  18191  ptcldmpt  19878  ptcnp  19886  cnmpt11  19927  cnmpt21  19935  cnmptk2  19950  prdsdsf  20633  prdsxmet  20635  ovolfiniun  21675  ovoliunlem3  21678  ovoliun  21679  ovoliun2  21680  ovoliunnul  21681  volfiniun  21720  voliun  21727  mbfsup  21834  mbflim  21838  itg2splitlem  21918  itg2split  21919  itg2cnlem1  21931  isibl2  21936  nfitg1  21943  nfitg  21944  cbvitg  21945  itgabs  22004  dvlipcn  22158  lhop2  22179  dvfsumabs  22187  dvfsumrlim  22195  itgparts  22211  itgsubstlem  22212  ulmss  22554  itgulm2  22566  lgseisenlem2  23381  dchrisumlem3  23432  cnlnadjlem5  26694  dfimafnf  27174  esumfzf  27743  voliune  27869  volfiniune  27870  lgamgulmlem2  28240  lgamgulmlem6  28244  lgamgulm2  28246  cvmcov  28376  nfcprod1  28647  nfcprod  28648  fprodefsum  28709  trpredlem1  28915  trpredrec  28926  nfwrecs  28943  sltval2  29021  nobndlem5  29061  itgabsnc  29689  mzpsubst  30313  aomclem8  30639  evth2f  30996  fvelrnbf  30999  evthf  31008  rfcnpre3  31014  rfcnpre4  31015  rfcnnnub  31017  refsum2cnlem1  31018  fmul01  31158  fmuldfeqlem1  31160  fmuldfeq  31161  fmul01lt1lem1  31162  fmul01lt1lem2  31163  fmul01lt1  31164  cncfmptss  31165  mulc1cncfg  31167  expcnfg  31170  climmulf  31174  climexp  31175  climsuse  31178  climrecf  31179  climinff  31181  climaddf  31185  mullimc  31186  idlimc  31196  limcperiod  31198  neglimc  31217  addlimc  31218  0ellimcdiv  31219  cncfshift  31240  icccncfext  31254  cncficcgt0  31255  cncfiooicclem1  31260  itgsubsticclem  31321  stoweidlem3  31331  stoweidlem23  31351  stoweidlem26  31354  stoweidlem28  31356  stoweidlem29  31357  stoweidlem31  31359  stoweidlem34  31362  stoweidlem36  31364  stoweidlem42  31370  stoweidlem48  31376  stoweidlem51  31379  stoweidlem52  31380  stoweidlem59  31387  wallispilem5  31397  stirlinglem4  31405  stirlinglem11  31412  stirlinglem12  31413  stirlinglem13  31414  stirlinglem14  31415  stirlinglem15  31416  fourierdlem20  31455  fourierdlem31  31466  fourierdlem79  31514  fourierdlem89  31524  fourierdlem91  31526  fourierdlem112  31547  fourierdlem115  31550  fourierd  31551  fourierclimd  31552  nfafv  31716  bnj1534  33008  bnj1542  33012  bnj958  33095  bnj1000  33096  bnj1446  33198  bnj1447  33199  bnj1448  33200  bnj1466  33206  bnj1467  33207  bnj1519  33218  bnj1520  33219  bnj1529  33223  riotaocN  34024  cdleme32d  35258  cdleme32f  35260  ltrniotaval  35395  cdlemksv2  35661  cdlemkuv2  35681  cdlemk36  35727  cdlemk38  35729  cdlemk19x  35757  cdlemk11t  35760
  Copyright terms: Public domain W3C validator