Theorem nffv 6902

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 6552	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2904	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5196	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6500	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2902	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2884   class class class wbr 5149  ℩cio 6494  ‘cfv 6544

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552

This theorem is referenced by:  nffvmpt1  6903  nffvd  6904  fvelimad  6960  dffn5f  6964  fvmptss  7011  fvmptex  7013  fvmptf  7020  fvmptnf  7021  eqfnfv2f  7037  ralrnmptw  7096  ralrnmpt  7098  ffnfvf  7119  funiunfvf  7248  dff13f  7255  nfiso  7319  nfwrecsOLD  8302  nfrdg  8414  rdgsucmptf  8428  rdgsucmptnf  8429  frsucmpt  8438  frsucmptn  8439  ttrclselem1  9720  ttrclselem2  9721  rankidb  9795  rankval4  9862  dfac8clem  10027  cardaleph  10084  hsmexlem2  10422  axcc2  10432  uniimadomf  10540  nfseq  13976  seqof2  14026  rlim2  15440  nfsum1  15636  nfsum  15637  sumeq2ii  15639  fsumrelem  15753  o1fsum  15759  nfcprod1  15854  nfcprod  15855  fprodefsum  16038  prdsbas3  17427  prdsdsval2  17430  yonedalem4b  18229  gsum2d2lem  19841  coe1fzgsumdlem  21825  evl1gsumdlem  21875  ptcldmpt  23118  ptcnp  23126  cnmpt11  23167  cnmpt21  23175  cnmptk2  23190  prdsdsf  23873  prdsxmet  23875  ovolfiniun  25018  ovoliunlem3  25021  ovoliun  25022  ovoliun2  25023  ovoliunnul  25024  volfiniun  25064  voliun  25071  mbfsup  25181  mbflim  25185  itg2splitlem  25266  itg2split  25267  itg2cnlem1  25279  isibl2  25284  nfitg1  25291  nfitg  25292  cbvitg  25293  itgabs  25352  dvlipcn  25511  lhop2  25532  dvfsumabs  25540  dvfsumrlim  25548  itgparts  25564  itgsubstlem  25565  ulmss  25909  itgulm2  25921  lgamgulmlem2  26534  lgamgulmlem6  26538  lgamgulm2  26540  lgseisenlem2  26879  dchrisumlem3  26994  sltval2  27159  cnlnadjlem5  31324  dfimafnf  31860  2ndresdju  31874  esumfzf  33067  voliune  33227  volfiniune  33228  bnj1534  33864  bnj1542  33868  bnj958  33951  bnj1000  33952  bnj1446  34056  bnj1447  34057  bnj1448  34058  bnj1466  34064  bnj1467  34065  bnj1519  34076  bnj1520  34077  bnj1529  34081  cvmcov  34254  rdgssun  36259  exrecfnlem  36260  finxpreclem2  36271  finxpreclem6  36277  poimirlem23  36511  poimirlem27  36515  itgabsnc  36557  riotaocN  38079  cdleme32d  39315  cdleme32f  39317  ltrniotaval  39452  cdlemksv2  39718  cdlemkuv2  39738  cdlemk36  39784  cdlemk38  39786  cdlemk19x  39814  cdlemk11t  39817  mzpsubst  41486  aomclem8  41803  mnringmulrcld  42987  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  evth2f  43699  fvelrnbf  43702  evthf  43711  rfcnpre3  43717  rfcnpre4  43718  rfcnnnub  43720  refsum2cnlem1  43721  dffo3f  43877  allbutfiinf  44130  monoordxr  44193  monoord2xr  44195  caucvgbf  44200  cvgcaule  44202  fmul01  44296  fmuldfeqlem1  44298  fmuldfeq  44299  fmul01lt1lem1  44300  fmul01lt1lem2  44301  fmul01lt1  44302  cncfmptss  44303  mulc1cncfg  44305  expcnfg  44307  fprodabs2  44311  climmulf  44320  climexp  44321  climsuse  44324  climrecf  44325  climinff  44327  climaddf  44331  mullimc  44332  idlimc  44342  limcperiod  44344  neglimc  44363  addlimc  44364  0ellimcdiv  44365  fnlimfv  44379  climreclf  44380  fnlimcnv  44383  fnlimfvre  44390  fnlimfvre2  44393  fnlimf  44394  fnlimabslt  44395  climfveqf  44396  climmptf  44397  climeldmeqf  44399  limsupref  44401  limsupbnd1f  44402  climbddf  44403  climeqf  44404  limsuppnfd  44418  climinf2  44423  limsuppnf  44427  limsupubuz  44429  climinfmpt  44431  limsupmnf  44437  limsupequz  44439  limsupre2  44441  limsupmnfuz  44443  limsupre3  44449  limsupre3uz  44452  limsupreuz  44453  climuz  44460  lmbr3  44463  limsupgt  44494  liminfvalxr  44499  liminfreuz  44519  liminflt  44521  xlimpnfxnegmnf  44530  liminfpnfuz  44532  xlimmnf  44557  xlimpnf  44558  dfxlim2  44564  xlimpnfxnegmnf2  44574  cncfshift  44590  icccncfext  44603  cncficcgt0  44604  cncfiooicclem1  44609  dvnmul  44659  dvnprodlem1  44662  itgsubsticclem  44691  stoweidlem3  44719  stoweidlem23  44739  stoweidlem26  44742  stoweidlem28  44744  stoweidlem29  44745  stoweidlem31  44747  stoweidlem34  44750  stoweidlem36  44752  stoweidlem42  44758  stoweidlem48  44764  stoweidlem51  44767  stoweidlem52  44768  stoweidlem59  44775  wallispilem5  44785  stirlinglem4  44793  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  fourierdlem20  44843  fourierdlem31  44854  fourierdlem79  44901  fourierdlem89  44911  fourierdlem91  44913  fourierdlem112  44934  fourierdlem115  44937  fourierd  44938  fourierclimd  44939  etransclem2  44952  etransclem48  44998  sge0revalmpt  45094  sge0fsummpt  45106  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  sge0xadd  45151  sge0fsummptf  45152  sge0gtfsumgt  45159  iundjiun  45176  meadjiun  45182  voliunsge0lem  45188  meaiunincf  45199  meaiuninc3  45201  omeiunle  45233  omeiunltfirp  45235  ovncvrrp  45280  vonioo  45398  vonicc  45401  vonn0ioo2  45406  vonn0icc2  45408  pimltmnf2f  45413  pimgtpnf2f  45421  pimltpnf2f  45428  pimgtmnf2  45430  pimdecfgtioc  45431  issmff  45450  smfpimltxrmptf  45474  smfpreimagtf  45484  smflim  45493  smfpimgtxr  45496  smfpimgtxrmptf  45500  smfmullem4  45510  smflim2  45522  smfpimcclem  45523  smfpimcc  45524  smfsup  45530  smfsupmpt  45531  smfsupxr  45532  smfinflem  45533  smfinf  45534  smfinfmpt  45535  smflimsuplem2  45537  smflimsuplem5  45540  smflimsuplem7  45542  smflimsup  45544  smfliminf  45547  fsupdm  45558  smfsupdmmbllem  45560  finfdm  45562  smfinfdmmbllem  45564  nfafv  45844  nfsetrecs  47731  setrec2fun  47737