Theorem nffv 6198

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.

Step	Hyp	Ref	Expression
1		df-fv 5896	. 2 |- ( F ` A ) = ( iota y A F y )
2		nffv.2	. . . 4 |- F/_ x A
3		nffv.1	. . . 4 |- F/_ x F
4		nfcv 2764	. . . 4 |- F/_ x y
5	2, 3, 4	nfbr 4699	. . 3 |- F/ x A F y
6	5	nfiota 5855	. 2 |- F/_ x ( iota y A F y )
7	1, 6	nfcxfr 2762	1 |- F/_ x ( F ` A )

Syntax hints:   F/_wnfc 2751   class class class wbr 4653   iotacio 5849   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896

This theorem is referenced by:  nffvmpt1  6199  nffvd  6200  dffn5f  6252  fvmptss  6292  fvmptex  6294  fvmptf  6301  fvmptnf  6302  eqfnfv2f  6315  ralrnmpt  6368  ffnfvf  6389  funiunfvf  6507  dff13f  6513  nfiso  6572  nfwrecs  7409  nfrdg  7510  rdgsucmptf  7524  rdgsucmptnf  7525  frsucmpt  7533  frsucmptn  7534  rankidb  8663  rankval4  8730  dfac8clem  8855  cardaleph  8912  hsmexlem2  9249  axcc2  9259  uniimadomf  9367  nfseq  12811  seqof2  12859  rlim2  14227  nfsum1  14420  nfsum  14421  sumeq2ii  14423  fsumrelem  14539  o1fsum  14545  nfcprod1  14640  nfcprod  14641  fprodefsum  14825  prdsbas3  16141  prdsdsval2  16144  yonedalem4b  16916  gsum2d2lem  18372  coe1fzgsumdlem  19671  evl1gsumdlem  19720  ptcldmpt  21417  ptcnp  21425  cnmpt11  21466  cnmpt21  21474  cnmptk2  21489  prdsdsf  22172  prdsxmet  22174  ovolfiniun  23269  ovoliunlem3  23272  ovoliun  23273  ovoliun2  23274  ovoliunnul  23275  volfiniun  23315  voliun  23322  mbfsup  23431  mbflim  23435  itg2splitlem  23515  itg2split  23516  itg2cnlem1  23528  isibl2  23533  nfitg1  23540  nfitg  23541  cbvitg  23542  itgabs  23601  dvlipcn  23757  lhop2  23778  dvfsumabs  23786  dvfsumrlim  23794  itgparts  23810  itgsubstlem  23811  ulmss  24151  itgulm2  24163  lgamgulmlem2  24756  lgamgulmlem6  24760  lgamgulm2  24762  lgseisenlem2  25101  dchrisumlem3  25180  cnlnadjlem5  28930  dfimafnf  29436  esumfzf  30131  voliune  30292  volfiniune  30293  bnj1534  30923  bnj1542  30927  bnj958  31010  bnj1000  31011  bnj1446  31113  bnj1447  31114  bnj1448  31115  bnj1466  31121  bnj1467  31122  bnj1519  31133  bnj1520  31134  bnj1529  31138  cvmcov  31245  trpredlem1  31727  trpredrec  31738  sltval2  31809  finxpreclem2  33227  finxpreclem6  33233  poimirlem23  33432  poimirlem27  33436  itgabsnc  33479  riotaocN  34496  cdleme32d  35732  cdleme32f  35734  ltrniotaval  35869  cdlemksv2  36135  cdlemkuv2  36155  cdlemk36  36201  cdlemk38  36203  cdlemk19x  36231  cdlemk11t  36234  mzpsubst  37311  aomclem8  37631  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  evth2f  39174  fvelrnbf  39177  evthf  39186  rfcnpre3  39192  rfcnpre4  39193  rfcnnnub  39195  refsum2cnlem1  39196  dffo3f  39364  fvelimad  39458  allbutfiinf  39647  fmul01  39812  fmuldfeqlem1  39814  fmuldfeq  39815  fmul01lt1lem1  39816  fmul01lt1lem2  39817  fmul01lt1  39818  cncfmptss  39819  mulc1cncfg  39821  expcnfg  39823  fprodabs2  39827  climmulf  39836  climexp  39837  climsuse  39840  climrecf  39841  climinff  39843  climaddf  39847  mullimc  39848  idlimc  39858  limcperiod  39860  neglimc  39879  addlimc  39880  0ellimcdiv  39881  fnlimfv  39895  climreclf  39896  fnlimcnv  39899  fnlimfvre  39906  fnlimfvre2  39909  fnlimf  39910  fnlimabslt  39911  climfveqf  39912  climmptf  39913  climeldmeqf  39915  limsupref  39917  limsupbnd1f  39918  climbddf  39919  climeqf  39920  limsuppnfd  39934  climinf2  39939  limsuppnf  39943  limsupubuz  39945  climinfmpt  39947  limsupmnf  39953  limsupequz  39955  limsupre2  39957  limsupmnfuz  39959  limsupre3  39965  limsupre3uz  39968  limsupreuz  39969  climuz  39976  lmbr3  39979  limsupgt  40010  liminfvalxr  40015  liminfreuz  40035  liminflt  40037  xlimmnf  40067  xlimpnf  40068  dfxlim2  40074  cncfshift  40087  icccncfext  40100  cncficcgt0  40101  cncfiooicclem1  40106  dvnmul  40158  dvnprodlem1  40161  itgsubsticclem  40191  stoweidlem3  40220  stoweidlem23  40240  stoweidlem26  40243  stoweidlem28  40245  stoweidlem29  40246  stoweidlem31  40248  stoweidlem34  40251  stoweidlem36  40253  stoweidlem42  40259  stoweidlem48  40265  stoweidlem51  40268  stoweidlem52  40269  stoweidlem59  40276  wallispilem5  40286  stirlinglem4  40294  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  fourierdlem20  40344  fourierdlem31  40355  fourierdlem79  40402  fourierdlem89  40412  fourierdlem91  40414  fourierdlem112  40435  fourierdlem115  40438  fourierd  40439  fourierclimd  40440  etransclem2  40453  etransclem48  40499  sge0revalmpt  40595  sge0fsummpt  40607  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0xadd  40652  sge0fsummptf  40653  sge0gtfsumgt  40660  iundjiun  40677  meadjiun  40683  voliunsge0lem  40689  omeiunle  40731  omeiunltfirp  40733  ovncvrrp  40778  vonioo  40896  vonicc  40899  vonn0ioo2  40904  vonn0icc2  40906  pimltmnf2  40911  pimgtpnf2  40917  pimltpnf2  40923  pimgtmnf2  40924  pimdecfgtioc  40925  issmff  40943  smfpimltxrmpt  40967  smfpreimagtf  40976  smflim  40985  smfpimgtxr  40988  smfpimgtxrmpt  40992  smfmullem4  41001  smflim2  41012  smfpimcclem  41013  smfpimcc  41014  smfsup  41020  smfsupmpt  41021  smfsupxr  41022  smfinflem  41023  smfinf  41024  smfinfmpt  41025  smflimsuplem2  41027  smflimsuplem5  41030  smflimsuplem7  41032  smflimsup  41034  smfliminf  41037  nfafv  41216  nfsetrecs  42433  setrec2fun  42439