Theorem nffv 6339

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 6039	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2913	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 4833	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiota 5998	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2911	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2900   class class class wbr 4786  ℩cio 5992  ‘cfv 6031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039

This theorem is referenced by:  nffvmpt1  6340  nffvd  6341  dffn5f  6394  fvmptss  6434  fvmptex  6436  fvmptf  6443  fvmptnf  6444  eqfnfv2f  6458  ralrnmpt  6511  ffnfvf  6531  funiunfvf  6650  dff13f  6656  nfiso  6715  nfwrecs  7561  nfrdg  7663  rdgsucmptf  7677  rdgsucmptnf  7678  frsucmpt  7686  frsucmptn  7687  rankidb  8827  rankval4  8894  dfac8clem  9055  cardaleph  9112  hsmexlem2  9451  axcc2  9461  uniimadomf  9569  nfseq  13018  seqof2  13066  rlim2  14435  nfsum1  14628  nfsum  14629  sumeq2ii  14631  fsumrelem  14746  o1fsum  14752  nfcprod1  14847  nfcprod  14848  fprodefsum  15031  prdsbas3  16349  prdsdsval2  16352  yonedalem4b  17124  gsum2d2lem  18579  coe1fzgsumdlem  19886  evl1gsumdlem  19935  ptcldmpt  21638  ptcnp  21646  cnmpt11  21687  cnmpt21  21695  cnmptk2  21710  prdsdsf  22392  prdsxmet  22394  ovolfiniun  23489  ovoliunlem3  23492  ovoliun  23493  ovoliun2  23494  ovoliunnul  23495  volfiniun  23535  voliun  23542  mbfsup  23651  mbflim  23655  itg2splitlem  23735  itg2split  23736  itg2cnlem1  23748  isibl2  23753  nfitg1  23760  nfitg  23761  cbvitg  23762  itgabs  23821  dvlipcn  23977  lhop2  23998  dvfsumabs  24006  dvfsumrlim  24014  itgparts  24030  itgsubstlem  24031  ulmss  24371  itgulm2  24383  lgamgulmlem2  24977  lgamgulmlem6  24981  lgamgulm2  24983  lgseisenlem2  25322  dchrisumlem3  25401  cnlnadjlem5  29270  dfimafnf  29776  esumfzf  30471  voliune  30632  volfiniune  30633  bnj1534  31261  bnj1542  31265  bnj958  31348  bnj1000  31349  bnj1446  31451  bnj1447  31452  bnj1448  31453  bnj1466  31459  bnj1467  31460  bnj1519  31471  bnj1520  31472  bnj1529  31476  cvmcov  31583  trpredlem1  32063  trpredrec  32074  sltval2  32146  finxpreclem2  33564  finxpreclem6  33570  poimirlem23  33765  poimirlem27  33769  itgabsnc  33811  riotaocN  35018  cdleme32d  36253  cdleme32f  36255  ltrniotaval  36390  cdlemksv2  36656  cdlemkuv2  36676  cdlemk36  36722  cdlemk38  36724  cdlemk19x  36752  cdlemk11t  36755  mzpsubst  37837  aomclem8  38157  binomcxplemdvbinom  39078  binomcxplemdvsum  39080  binomcxplemnotnn0  39081  evth2f  39696  fvelrnbf  39699  evthf  39708  rfcnpre3  39714  rfcnpre4  39715  rfcnnnub  39717  refsum2cnlem1  39718  dffo3f  39884  fvelimad  39976  allbutfiinf  40163  monoordxr  40229  monoord2xr  40231  fmul01  40330  fmuldfeqlem1  40332  fmuldfeq  40333  fmul01lt1lem1  40334  fmul01lt1lem2  40335  fmul01lt1  40336  cncfmptss  40337  mulc1cncfg  40339  expcnfg  40341  fprodabs2  40345  climmulf  40354  climexp  40355  climsuse  40358  climrecf  40359  climinff  40361  climaddf  40365  mullimc  40366  idlimc  40376  limcperiod  40378  neglimc  40397  addlimc  40398  0ellimcdiv  40399  fnlimfv  40413  climreclf  40414  fnlimcnv  40417  fnlimfvre  40424  fnlimfvre2  40427  fnlimf  40428  fnlimabslt  40429  climfveqf  40430  climmptf  40431  climeldmeqf  40433  limsupref  40435  limsupbnd1f  40436  climbddf  40437  climeqf  40438  limsuppnfd  40452  climinf2  40457  limsuppnf  40461  limsupubuz  40463  climinfmpt  40465  limsupmnf  40471  limsupequz  40473  limsupre2  40475  limsupmnfuz  40477  limsupre3  40483  limsupre3uz  40486  limsupreuz  40487  climuz  40494  lmbr3  40497  limsupgt  40528  liminfvalxr  40533  liminfreuz  40553  liminflt  40555  xlimmnf  40585  xlimpnf  40586  dfxlim2  40592  cncfshift  40605  icccncfext  40618  cncficcgt0  40619  cncfiooicclem1  40624  dvnmul  40676  dvnprodlem1  40679  itgsubsticclem  40708  stoweidlem3  40737  stoweidlem23  40757  stoweidlem26  40760  stoweidlem28  40762  stoweidlem29  40763  stoweidlem31  40765  stoweidlem34  40768  stoweidlem36  40770  stoweidlem42  40776  stoweidlem48  40782  stoweidlem51  40785  stoweidlem52  40786  stoweidlem59  40793  wallispilem5  40803  stirlinglem4  40811  stirlinglem11  40818  stirlinglem12  40819  stirlinglem13  40820  stirlinglem14  40821  stirlinglem15  40822  fourierdlem20  40861  fourierdlem31  40872  fourierdlem79  40919  fourierdlem89  40929  fourierdlem91  40931  fourierdlem112  40952  fourierdlem115  40955  fourierd  40956  fourierclimd  40957  etransclem2  40970  etransclem48  41016  sge0revalmpt  41112  sge0fsummpt  41124  sge0iunmptlemfi  41147  sge0iunmptlemre  41149  sge0iunmpt  41152  sge0xadd  41169  sge0fsummptf  41170  sge0gtfsumgt  41177  iundjiun  41194  meadjiun  41200  voliunsge0lem  41206  meaiunincf  41217  meaiuninc3  41219  omeiunle  41251  omeiunltfirp  41253  ovncvrrp  41298  vonioo  41416  vonicc  41419  vonn0ioo2  41424  vonn0icc2  41426  pimltmnf2  41431  pimgtpnf2  41437  pimltpnf2  41443  pimgtmnf2  41444  pimdecfgtioc  41445  issmff  41463  smfpimltxrmpt  41487  smfpreimagtf  41496  smflim  41505  smfpimgtxr  41508  smfpimgtxrmpt  41512  smfmullem4  41521  smflim2  41532  smfpimcclem  41533  smfpimcc  41534  smfsup  41540  smfsupmpt  41541  smfsupxr  41542  smfinflem  41543  smfinf  41544  smfinfmpt  41545  smflimsuplem2  41547  smflimsuplem5  41550  smflimsuplem7  41552  smflimsup  41554  smfliminf  41557  nfafv  41736  nfsetrecs  42961  setrec2fun  42967