Theorem nffv 6793

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	⊢ Ⅎ𝑥𝐹
nffv.2	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nffv	⊢ Ⅎ𝑥(𝐹‘𝐴)

Proof of Theorem nffv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 6445	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2908	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5122	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6399	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2906	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2888   class class class wbr 5075  ℩cio 6393  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445

This theorem is referenced by:  nffvmpt1  6794  nffvd  6795  fvelimad  6845  dffn5f  6849  fvmptss  6896  fvmptex  6898  fvmptf  6905  fvmptnf  6906  eqfnfv2f  6922  ralrnmptw  6979  ralrnmpt  6981  ffnfvf  7002  funiunfvf  7131  dff13f  7138  nfiso  7202  nfwrecsOLD  8142  nfrdg  8254  rdgsucmptf  8268  rdgsucmptnf  8269  frsucmpt  8278  frsucmptn  8279  ttrclselem1  9492  ttrclselem2  9493  rankidb  9567  rankval4  9634  dfac8clem  9797  cardaleph  9854  hsmexlem2  10192  axcc2  10202  uniimadomf  10310  nfseq  13740  seqof2  13790  rlim2  15214  nfsum1  15410  nfsum  15411  nfsumOLD  15412  sumeq2ii  15414  fsumrelem  15528  o1fsum  15534  nfcprod1  15629  nfcprod  15630  fprodefsum  15813  prdsbas3  17201  prdsdsval2  17204  yonedalem4b  18003  gsum2d2lem  19583  coe1fzgsumdlem  21481  evl1gsumdlem  21531  ptcldmpt  22774  ptcnp  22782  cnmpt11  22823  cnmpt21  22831  cnmptk2  22846  prdsdsf  23529  prdsxmet  23531  ovolfiniun  24674  ovoliunlem3  24677  ovoliun  24678  ovoliun2  24679  ovoliunnul  24680  volfiniun  24720  voliun  24727  mbfsup  24837  mbflim  24841  itg2splitlem  24922  itg2split  24923  itg2cnlem1  24935  isibl2  24940  nfitg1  24947  nfitg  24948  cbvitg  24949  itgabs  25008  dvlipcn  25167  lhop2  25188  dvfsumabs  25196  dvfsumrlim  25204  itgparts  25220  itgsubstlem  25221  ulmss  25565  itgulm2  25577  lgamgulmlem2  26188  lgamgulmlem6  26192  lgamgulm2  26194  lgseisenlem2  26533  dchrisumlem3  26648  cnlnadjlem5  30442  dfimafnf  30980  2ndresdju  30995  esumfzf  32046  voliune  32206  volfiniune  32207  bnj1534  32842  bnj1542  32846  bnj958  32929  bnj1000  32930  bnj1446  33034  bnj1447  33035  bnj1448  33036  bnj1466  33042  bnj1467  33043  bnj1519  33054  bnj1520  33055  bnj1529  33059  cvmcov  33234  sltval2  33868  rdgssun  35558  exrecfnlem  35559  finxpreclem2  35570  finxpreclem6  35576  poimirlem23  35809  poimirlem27  35813  itgabsnc  35855  riotaocN  37230  cdleme32d  38465  cdleme32f  38467  ltrniotaval  38602  cdlemksv2  38868  cdlemkuv2  38888  cdlemk36  38934  cdlemk38  38936  cdlemk19x  38964  cdlemk11t  38967  mzpsubst  40577  aomclem8  40893  mnringmulrcld  41853  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  evth2f  42565  fvelrnbf  42568  evthf  42577  rfcnpre3  42583  rfcnpre4  42584  rfcnnnub  42586  refsum2cnlem1  42587  dffo3f  42724  allbutfiinf  42967  monoordxr  43030  monoord2xr  43032  fmul01  43128  fmuldfeqlem1  43130  fmuldfeq  43131  fmul01lt1lem1  43132  fmul01lt1lem2  43133  fmul01lt1  43134  cncfmptss  43135  mulc1cncfg  43137  expcnfg  43139  fprodabs2  43143  climmulf  43152  climexp  43153  climsuse  43156  climrecf  43157  climinff  43159  climaddf  43163  mullimc  43164  idlimc  43174  limcperiod  43176  neglimc  43195  addlimc  43196  0ellimcdiv  43197  fnlimfv  43211  climreclf  43212  fnlimcnv  43215  fnlimfvre  43222  fnlimfvre2  43225  fnlimf  43226  fnlimabslt  43227  climfveqf  43228  climmptf  43229  climeldmeqf  43231  limsupref  43233  limsupbnd1f  43234  climbddf  43235  climeqf  43236  limsuppnfd  43250  climinf2  43255  limsuppnf  43259  limsupubuz  43261  climinfmpt  43263  limsupmnf  43269  limsupequz  43271  limsupre2  43273  limsupmnfuz  43275  limsupre3  43281  limsupre3uz  43284  limsupreuz  43285  climuz  43292  lmbr3  43295  limsupgt  43326  liminfvalxr  43331  liminfreuz  43351  liminflt  43353  xlimpnfxnegmnf  43362  liminfpnfuz  43364  xlimmnf  43389  xlimpnf  43390  dfxlim2  43396  xlimpnfxnegmnf2  43406  cncfshift  43422  icccncfext  43435  cncficcgt0  43436  cncfiooicclem1  43441  dvnmul  43491  dvnprodlem1  43494  itgsubsticclem  43523  stoweidlem3  43551  stoweidlem23  43571  stoweidlem26  43574  stoweidlem28  43576  stoweidlem29  43577  stoweidlem31  43579  stoweidlem34  43582  stoweidlem36  43584  stoweidlem42  43590  stoweidlem48  43596  stoweidlem51  43599  stoweidlem52  43600  stoweidlem59  43607  wallispilem5  43617  stirlinglem4  43625  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  fourierdlem20  43675  fourierdlem31  43686  fourierdlem79  43733  fourierdlem89  43743  fourierdlem91  43745  fourierdlem112  43766  fourierdlem115  43769  fourierd  43770  fourierclimd  43771  etransclem2  43784  etransclem48  43830  sge0revalmpt  43923  sge0fsummpt  43935  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0xadd  43980  sge0fsummptf  43981  sge0gtfsumgt  43988  iundjiun  44005  meadjiun  44011  voliunsge0lem  44017  meaiunincf  44028  meaiuninc3  44030  omeiunle  44062  omeiunltfirp  44064  ovncvrrp  44109  vonioo  44227  vonicc  44230  vonn0ioo2  44235  vonn0icc2  44237  pimltmnf2f  44242  pimgtpnf2f  44250  pimltpnf2f  44257  pimgtmnf2  44259  pimdecfgtioc  44260  issmff  44279  smfpimltxrmptf  44303  smfpreimagtf  44313  smflim  44322  smfpimgtxr  44325  smfpimgtxrmptf  44329  smfmullem4  44339  smflim2  44350  smfpimcclem  44351  smfpimcc  44352  smfsup  44358  smfsupmpt  44359  smfsupxr  44360  smfinflem  44361  smfinf  44362  smfinfmpt  44363  smflimsuplem2  44365  smflimsuplem5  44368  smflimsuplem7  44370  smflimsup  44372  smfliminf  44375  nfafv  44639  nfsetrecs  46403  setrec2fun  46409