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

Theorem nffv 5615
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 5345 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2494 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4148 . . 3  |-  F/ x  A F y
65nfiota 5305 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2491 1  |-  F/_ x
( F `  A
)
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2481   class class class wbr 4104   iotacio 5299   ` cfv 5337
This theorem is referenced by:  nffvmpt1  5616  nffvd  5617  dffn5f  5660  fvmptss  5692  fvmptex  5693  fvmptt  5698  fvmptf  5699  fvmptnf  5700  eqfnfv2f  5709  ralrnmpt  5752  ffnfvf  5769  fmptco  5774  funiunfvf  5862  dff13f  5871  nfiso  5908  offval2  6182  ofrfval2  6183  opabiota  6380  nfriota1  6399  nfrecs  6477  nfrdg  6514  rdgsucmptf  6528  rdgsucmptnf  6529  frsucmpt  6537  frsucmptn  6538  mptelixpg  6941  dom2lem  6989  rankidb  7562  rankval4  7629  dfac8clem  7749  acni2  7763  cardaleph  7806  hsmexlem2  8143  axcc2  8153  axdclem  8236  uniimadomf  8257  nfseq  11148  seqof2  11196  rlim2  12066  ello1mpt  12091  o1compt  12157  nfsum1  12260  nfsum  12261  sumfc  12279  zsum  12288  fsum  12290  fsumf1o  12293  sumss  12294  fsumcvg2  12297  fsumadd  12308  isummulc2  12322  fsummulc2  12343  fsumrelem  12362  o1fsum  12368  isumshft  12395  iserodd  12985  prdsbas3  13479  prdsdsval2  13482  yonedalem4b  14149  gsum2d2lem  15323  dprdwd  15345  gsumdixp  15491  evlslem4  16344  elptr2  17375  ptunimpt  17396  ptcldmpt  17414  ptclsg  17415  txcnp  17420  ptcnplem  17421  ptcnp  17422  cnmpt11  17463  cnmpt1t  17465  cnmpt21  17471  cnmptk2  17486  flfcnp2  17804  prdsdsf  18033  prdsxmet  18035  ovolfiniun  18964  ovoliunlem3  18967  ovoliun  18968  ovoliun2  18969  ovoliunnul  18970  volfiniun  19008  voliun  19015  mbfeqalem  19101  mbfpos  19110  mbfposb  19112  mbfsup  19123  mbfinf  19124  mbflim  19127  i1fposd  19166  itg2splitlem  19207  itg2split  19208  itg2cnlem1  19220  isibl2  19225  nfitg1  19232  nfitg  19233  cbvitg  19234  itgmpt  19241  itgeqa  19272  itgabs  19293  itggt0  19300  itgcn  19301  dvlipcn  19445  lhop2  19466  dvfsumabs  19474  dvfsumrlim  19482  itgparts  19498  itgsubstlem  19499  itgsubst  19500  elplyd  19688  coeeq2  19728  dgrle  19729  ulmss  19880  itgulm2  19892  leibpi  20349  rlimcnp  20371  o1cxp  20380  lgseisenlem2  20701  dchrisumlem3  20752  cnlnadjlem5  22765  dfimafnf  23247  fmptcof2  23280  offval2f  23284  esumfzf  23725  voliune  23849  volfiniune  23850  lgamgulmlem2  24063  lgamgulmlem6  24067  lgamgulm2  24069  cvmcov  24198  nfcprod1  24537  nfcprod  24538  zprod  24564  prodfc  24572  fprodf1o  24573  fprodefsum  24599  trpredlem1  24788  trpredrec  24799  sltval2  24868  nobndlem5  24908  itgabsnc  25509  ftc1cnnclem  25513  elrfirn2  26094  mzpsubst  26149  eq0rabdioph  26179  monotoddzz  26351  aomclem8  26482  evth2f  27009  fvelrnbf  27012  evthf  27021  rfcnpre3  27027  rfcnpre4  27028  rfcnnnub  27030  refsum2cnlem1  27031  fmul01  27033  fmuldfeqlem1  27035  fmuldfeq  27036  fmul01lt1lem1  27037  fmul01lt1lem2  27038  fmul01lt1  27039  cncfmptss  27040  mulc1cncfg  27044  expcnfg  27049  climmulf  27053  climexp  27054  climsuse  27057  climrecf  27058  climinff  27060  stoweidlem3  27075  stoweidlem23  27095  stoweidlem26  27098  stoweidlem28  27100  stoweidlem29  27101  stoweidlem31  27103  stoweidlem34  27106  stoweidlem36  27108  stoweidlem42  27114  stoweidlem48  27120  stoweidlem51  27123  stoweidlem52  27124  stoweidlem59  27131  wallispilem5  27141  stirlinglem4  27149  stirlinglem11  27156  stirlinglem12  27157  stirlinglem13  27158  stirlinglem14  27159  stirlinglem15  27160  nfafv  27324  bnj1534  28647  bnj1542  28651  bnj958  28734  bnj1000  28735  bnj1446  28837  bnj1447  28838  bnj1448  28839  bnj1466  28845  bnj1467  28846  bnj1519  28857  bnj1520  28858  bnj1529  28862  riotaocN  29468  cdleme32d  30702  cdleme32f  30704  ltrniotaval  30839  cdlemksv2  31105  cdlemkuv2  31125  cdlemk36  31171  cdlemk38  31173  cdlemk19x  31201  cdlemk11t  31204
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345
  Copyright terms: Public domain W3C validator