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

Theorem nffv 5532
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 5263 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2419 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4067 . . 3  |-  F/ x  A F y
65nfiota 5223 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2416 1  |-  F/_ x
( F `  A
)
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2406   class class class wbr 4023   iotacio 5217   ` cfv 5255
This theorem is referenced by:  nffvmpt1  5533  nffvd  5534  dffn5f  5577  fvmptss  5609  fvmptex  5610  fvmptt  5615  fvmptf  5616  fvmptnf  5617  eqfnfv2f  5626  ralrnmpt  5669  ffnfvf  5686  fmptco  5691  funiunfvf  5775  dff13f  5784  nfiso  5821  offval2  6095  ofrfval2  6096  opabiota  6293  nfriota1  6312  nfrecs  6390  nfrdg  6427  rdgsucmptf  6441  rdgsucmptnf  6442  frsucmpt  6450  frsucmptn  6451  mptelixpg  6853  dom2lem  6901  rankidb  7472  rankval4  7539  dfac8clem  7659  acni2  7673  cardaleph  7716  hsmexlem2  8053  axcc2  8063  axdclem  8146  uniimadomf  8167  nfseq  11056  rlim2  11970  ello1mpt  11995  o1compt  12061  nfsum1  12163  nfsum  12164  sumfc  12182  zsum  12191  fsum  12193  fsumf1o  12196  sumss  12197  fsumcvg2  12200  fsumadd  12211  isummulc2  12225  fsummulc2  12246  fsumrelem  12265  o1fsum  12271  isumshft  12298  iserodd  12888  prdsbas3  13380  prdsdsval2  13383  yonedalem4b  14050  gsum2d2lem  15224  dprdwd  15246  gsumdixp  15392  evlslem4  16245  elptr2  17269  ptunimpt  17290  ptcldmpt  17308  ptclsg  17309  txcnp  17314  ptcnplem  17315  ptcnp  17316  cnmpt11  17357  cnmpt1t  17359  cnmpt21  17365  cnmptk2  17380  flfcnp2  17702  prdsdsf  17931  prdsxmet  17933  ovolfiniun  18860  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  ovoliunnul  18866  volfiniun  18904  voliun  18911  mbfeqalem  18997  mbfpos  19006  mbfposb  19008  mbfsup  19019  mbfinf  19020  mbflim  19023  i1fposd  19062  itg2splitlem  19103  itg2split  19104  itg2cnlem1  19116  isibl2  19121  nfitg1  19128  nfitg  19129  cbvitg  19130  itgmpt  19137  itgeqa  19168  itgabs  19189  itggt0  19196  itgcn  19197  dvlipcn  19341  lhop2  19362  dvfsumabs  19370  dvfsumrlim  19378  itgparts  19394  itgsubstlem  19395  itgsubst  19396  elplyd  19584  coeeq2  19624  dgrle  19625  ulmss  19774  itgulm2  19785  leibpi  20238  rlimcnp  20260  o1cxp  20269  lgseisenlem2  20589  dchrisumlem3  20640  cnlnadjlem5  22651  dfimafnf  23041  fmptcof2  23229  offval2f  23233  cvmcov  23794  trpredlem1  24230  trpredrec  24241  sltval2  24310  nobndlem5  24350  prodeq3ii  25308  nfprod1  25310  nfprod  25311  prodeqfv  25318  fprodserf  25321  fprodadd  25352  fprodneg  25378  fprodsub  25379  intopcoaconb  25540  elrfirn2  26771  mzpsubst  26826  eq0rabdioph  26856  monotoddzz  27028  aomclem8  27159  evth2f  27686  fvelrnbf  27689  evthf  27698  rfcnpre3  27704  rfcnpre4  27705  rfcnnnub  27707  refsum2cnlem1  27708  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  fmul01lt1  27716  cncfmptss  27717  mulc1cncfg  27721  expcnfg  27726  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  climinff  27737  stoweidlem3  27752  stoweidlem23  27772  stoweidlem26  27775  stoweidlem28  27777  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem36  27785  stoweidlem42  27791  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem59  27808  wallispilem5  27818  stirlinglem4  27826  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  nfafv  27999  bnj1534  28885  bnj1542  28889  bnj958  28972  bnj1000  28973  bnj1446  29075  bnj1447  29076  bnj1448  29077  bnj1466  29083  bnj1467  29084  bnj1519  29095  bnj1520  29096  bnj1529  29100  riotaocN  29399  cdleme32d  30633  cdleme32f  30635  ltrniotaval  30770  cdlemksv2  31036  cdlemkuv2  31056  cdlemk36  31102  cdlemk38  31104  cdlemk19x  31132  cdlemk11t  31135
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-3an 936  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-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator