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

Theorem nffv 5855
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 5578 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2616 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4483 . . 3  |-  F/ x  A F y
65nfiota 5538 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2614 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2602   class class class wbr 4439   iotacio 5532   ` cfv 5570
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-3an 973  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-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578
This theorem is referenced by:  nffvmpt1  5856  nffvd  5857  dffn5f  5903  fvmptss  5940  fvmptex  5942  fvmptf  5948  fvmptnf  5949  eqfnfv2f  5961  ralrnmpt  6016  ffnfvf  6034  funiunfvf  6136  dff13f  6142  nfiso  6195  nfrecs  7036  nfrdg  7072  rdgsucmptf  7086  rdgsucmptnf  7087  frsucmpt  7095  frsucmptn  7096  rankidb  8209  rankval4  8276  dfac8clem  8404  cardaleph  8461  hsmexlem2  8798  axcc2  8808  uniimadomf  8911  nfseq  12099  seqof2  12147  rlim2  13401  nfsum1  13594  nfsum  13595  sumeq2ii  13597  fsumrelem  13703  o1fsum  13709  nfcprod1  13799  nfcprod  13800  fprodefsum  13912  prdsbas3  14970  prdsdsval2  14973  yonedalem4b  15744  gsum2d2lem  17197  coe1fzgsumdlem  18538  evl1gsumdlem  18587  ptcldmpt  20281  ptcnp  20289  cnmpt11  20330  cnmpt21  20338  cnmptk2  20353  prdsdsf  21036  prdsxmet  21038  ovolfiniun  22078  ovoliunlem3  22081  ovoliun  22082  ovoliun2  22083  ovoliunnul  22084  volfiniun  22123  voliun  22130  mbfsup  22237  mbflim  22241  itg2splitlem  22321  itg2split  22322  itg2cnlem1  22334  isibl2  22339  nfitg1  22346  nfitg  22347  cbvitg  22348  itgabs  22407  dvlipcn  22561  lhop2  22582  dvfsumabs  22590  dvfsumrlim  22598  itgparts  22614  itgsubstlem  22615  ulmss  22958  itgulm2  22970  lgseisenlem2  23823  dchrisumlem3  23874  cnlnadjlem5  27188  dfimafnf  27694  esumfzf  28298  voliune  28438  volfiniune  28439  lgamgulmlem2  28836  lgamgulmlem6  28840  lgamgulm2  28842  cvmcov  28972  trpredlem1  29550  trpredrec  29561  nfwrecs  29578  sltval2  29656  nobndlem5  29696  itgabsnc  30324  mzpsubst  30920  aomclem8  31246  binomcxplemdvbinom  31499  binomcxplemdvsum  31501  binomcxplemnotnn0  31502  evth2f  31630  fvelrnbf  31633  evthf  31642  rfcnpre3  31648  rfcnpre4  31649  rfcnnnub  31651  refsum2cnlem1  31652  fmul01  31813  fmuldfeqlem1  31815  fmuldfeq  31816  fmul01lt1lem1  31817  fmul01lt1lem2  31818  fmul01lt1  31819  cncfmptss  31820  mulc1cncfg  31822  expcnfg  31825  fprodabs2  31841  climmulf  31849  climexp  31850  climsuse  31853  climrecf  31854  climinff  31856  climaddf  31860  mullimc  31861  idlimc  31871  limcperiod  31873  neglimc  31892  addlimc  31893  0ellimcdiv  31894  cncfshift  31915  icccncfext  31929  cncficcgt0  31930  cncfiooicclem1  31935  dvnmul  31979  dvnprodlem1  31982  itgsubsticclem  32013  stoweidlem3  32024  stoweidlem23  32044  stoweidlem26  32047  stoweidlem28  32049  stoweidlem29  32050  stoweidlem31  32052  stoweidlem34  32055  stoweidlem36  32057  stoweidlem42  32063  stoweidlem48  32069  stoweidlem51  32072  stoweidlem52  32073  stoweidlem59  32080  wallispilem5  32090  stirlinglem4  32098  stirlinglem11  32105  stirlinglem12  32106  stirlinglem13  32107  stirlinglem14  32108  stirlinglem15  32109  fourierdlem20  32148  fourierdlem31  32159  fourierdlem79  32207  fourierdlem89  32217  fourierdlem91  32219  fourierdlem112  32240  fourierdlem115  32243  fourierd  32244  fourierclimd  32245  etransclem2  32258  etransclem48  32304  nfafv  32460  bnj1534  34312  bnj1542  34316  bnj958  34399  bnj1000  34400  bnj1446  34502  bnj1447  34503  bnj1448  34504  bnj1466  34510  bnj1467  34511  bnj1519  34522  bnj1520  34523  bnj1529  34527  riotaocN  35331  cdleme32d  36567  cdleme32f  36569  ltrniotaval  36704  cdlemksv2  36970  cdlemkuv2  36990  cdlemk36  37036  cdlemk38  37038  cdlemk19x  37066  cdlemk11t  37069
  Copyright terms: Public domain W3C validator