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

Theorem nffv 5548
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 5279 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2432 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4083 . . 3  |-  F/ x  A F y
65nfiota 5239 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2429 1  |-  F/_ x
( F `  A
)
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2419   class class class wbr 4039   iotacio 5233   ` cfv 5271
This theorem is referenced by:  nffvmpt1  5549  nffvd  5550  dffn5f  5593  fvmptss  5625  fvmptex  5626  fvmptt  5631  fvmptf  5632  fvmptnf  5633  eqfnfv2f  5642  ralrnmpt  5685  ffnfvf  5702  fmptco  5707  funiunfvf  5791  dff13f  5800  nfiso  5837  offval2  6111  ofrfval2  6112  opabiota  6309  nfriota1  6328  nfrecs  6406  nfrdg  6443  rdgsucmptf  6457  rdgsucmptnf  6458  frsucmpt  6466  frsucmptn  6467  mptelixpg  6869  dom2lem  6917  rankidb  7488  rankval4  7555  dfac8clem  7675  acni2  7689  cardaleph  7732  hsmexlem2  8069  axcc2  8079  axdclem  8162  uniimadomf  8183  nfseq  11072  rlim2  11986  ello1mpt  12011  o1compt  12077  nfsum1  12179  nfsum  12180  sumfc  12198  zsum  12207  fsum  12209  fsumf1o  12212  sumss  12213  fsumcvg2  12216  fsumadd  12227  isummulc2  12241  fsummulc2  12262  fsumrelem  12281  o1fsum  12287  isumshft  12314  iserodd  12904  prdsbas3  13396  prdsdsval2  13399  yonedalem4b  14066  gsum2d2lem  15240  dprdwd  15262  gsumdixp  15408  evlslem4  16261  elptr2  17285  ptunimpt  17306  ptcldmpt  17324  ptclsg  17325  txcnp  17330  ptcnplem  17331  ptcnp  17332  cnmpt11  17373  cnmpt1t  17375  cnmpt21  17381  cnmptk2  17396  flfcnp2  17718  prdsdsf  17947  prdsxmet  17949  ovolfiniun  18876  ovoliunlem3  18879  ovoliun  18880  ovoliun2  18881  ovoliunnul  18882  volfiniun  18920  voliun  18927  mbfeqalem  19013  mbfpos  19022  mbfposb  19024  mbfsup  19035  mbfinf  19036  mbflim  19039  i1fposd  19078  itg2splitlem  19119  itg2split  19120  itg2cnlem1  19132  isibl2  19137  nfitg1  19144  nfitg  19145  cbvitg  19146  itgmpt  19153  itgeqa  19184  itgabs  19205  itggt0  19212  itgcn  19213  dvlipcn  19357  lhop2  19378  dvfsumabs  19386  dvfsumrlim  19394  itgparts  19410  itgsubstlem  19411  itgsubst  19412  elplyd  19600  coeeq2  19640  dgrle  19641  ulmss  19790  itgulm2  19801  leibpi  20254  rlimcnp  20276  o1cxp  20285  lgseisenlem2  20605  dchrisumlem3  20656  cnlnadjlem5  22667  dfimafnf  23057  fmptcof2  23244  offval2f  23248  cvmcov  23809  nfcprod1  24132  nfcprod  24133  zprod  24160  prodfc  24171  fprodf1o  24172  trpredlem1  24301  trpredrec  24312  sltval2  24381  nobndlem5  24421  itgabsnc  25020  ftc1cnnclem  25024  prodeq3ii  25411  nfprod1  25413  nfprod  25414  prodeqfv  25421  fprodserf  25424  fprodadd  25455  fprodneg  25481  fprodsub  25482  intopcoaconb  25643  elrfirn2  26874  mzpsubst  26929  eq0rabdioph  26959  monotoddzz  27131  aomclem8  27262  evth2f  27789  fvelrnbf  27792  evthf  27801  rfcnpre3  27807  rfcnpre4  27808  rfcnnnub  27810  refsum2cnlem1  27811  fmul01  27813  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  fmul01lt1  27819  cncfmptss  27820  mulc1cncfg  27824  expcnfg  27829  climmulf  27833  climexp  27834  climsuse  27837  climrecf  27838  climinff  27840  stoweidlem3  27855  stoweidlem23  27875  stoweidlem26  27878  stoweidlem28  27880  stoweidlem29  27881  stoweidlem31  27883  stoweidlem34  27886  stoweidlem36  27888  stoweidlem42  27894  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem59  27911  wallispilem5  27921  stirlinglem4  27929  stirlinglem11  27936  stirlinglem12  27937  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  nfafv  28104  bnj1534  29201  bnj1542  29205  bnj958  29288  bnj1000  29289  bnj1446  29391  bnj1447  29392  bnj1448  29393  bnj1466  29399  bnj1467  29400  bnj1519  29411  bnj1520  29412  bnj1529  29416  riotaocN  30021  cdleme32d  31255  cdleme32f  31257  ltrniotaval  31392  cdlemksv2  31658  cdlemkuv2  31678  cdlemk36  31724  cdlemk38  31726  cdlemk19x  31754  cdlemk11t  31757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator