Theorem nffv 6844

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

Syntax hints:  Ⅎwnfc 2883   class class class wbr 5098  ℩cio 6446  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500

This theorem is referenced by:  nffvmpt1  6845  nffvd  6846  fvelimad  6901  dffn5f  6905  fvmptss  6953  fvmptex  6955  fvmptf  6962  fvmptnf  6963  eqfnfv2f  6980  ralrnmptw  7039  ralrnmpt  7041  dffo3f  7051  ffnfvf  7065  funiunfvf  7195  dff13f  7201  nfiso  7268  nfrdg  8345  rdgsucmptf  8359  rdgsucmptnf  8360  frsucmpt  8369  frsucmptn  8370  ttrclselem1  9634  ttrclselem2  9635  rankidb  9712  rankval4  9779  dfac8clem  9942  cardaleph  9999  hsmexlem2  10337  axcc2  10347  uniimadomf  10455  nfseq  13934  seqof2  13983  rlim2  15419  nfsum1  15613  nfsum  15614  sumeq2ii  15616  fsumrelem  15730  o1fsum  15736  nfcprod1  15831  nfcprod  15832  fprodefsum  16018  prdsbas3  17401  prdsdsval2  17404  yonedalem4b  18199  gsum2d2lem  19902  coe1fzgsumdlem  22247  evl1gsumdlem  22300  ptcldmpt  23558  ptcnp  23566  cnmpt11  23607  cnmpt21  23615  cnmptk2  23630  prdsdsf  24311  prdsxmet  24313  ovolfiniun  25458  ovoliunlem3  25461  ovoliun  25462  ovoliun2  25463  ovoliunnul  25464  volfiniun  25504  voliun  25511  mbfsup  25621  mbflim  25625  itg2splitlem  25705  itg2split  25706  itg2cnlem1  25718  isibl2  25723  nfitg1  25731  nfitg  25732  cbvitg  25733  itgabs  25792  dvlipcn  25955  lhop2  25976  dvfsumabs  25985  dvfsumrlim  25994  itgparts  26010  itgsubstlem  26011  ulmss  26362  itgulm2  26374  lgamgulmlem2  26996  lgamgulmlem6  27000  lgamgulm2  27002  lgseisenlem2  27343  dchrisumlem3  27458  ltsval2  27624  nfseqs  28283  cnlnadjlem5  32146  dfimafnf  32714  2ndresdju  32727  deg1prod  33664  esumfzf  34226  voliune  34386  volfiniune  34387  bnj1534  35009  bnj1542  35013  bnj958  35096  bnj1000  35097  bnj1446  35201  bnj1447  35202  bnj1448  35203  bnj1466  35209  bnj1467  35210  bnj1519  35221  bnj1520  35222  bnj1529  35226  rankval4b  35256  onvf1odlem2  35298  cvmcov  35457  rdgssun  37583  exrecfnlem  37584  finxpreclem2  37595  finxpreclem6  37601  poimirlem23  37844  poimirlem27  37848  itgabsnc  37890  riotaocN  39469  cdleme32d  40704  cdleme32f  40706  ltrniotaval  40841  cdlemksv2  41107  cdlemkuv2  41127  cdlemk36  41173  cdlemk38  41175  cdlemk19x  41203  cdlemk11t  41206  evl1gprodd  42371  mzpsubst  42990  aomclem8  43303  mnringmulrcld  44469  binomcxplemdvbinom  44594  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  nfrelp  45190  permaxrep  45247  permaxsep  45248  evth2f  45260  fvelrnbf  45263  evthf  45272  rfcnpre3  45278  rfcnpre4  45279  rfcnnnub  45281  refsum2cnlem1  45282  allbutfiinf  45664  monoordxr  45726  monoord2xr  45728  caucvgbf  45733  cvgcaule  45735  fmul01  45826  fmuldfeqlem1  45828  fmuldfeq  45829  fmul01lt1lem1  45830  fmul01lt1lem2  45831  fmul01lt1  45832  cncfmptss  45833  mulc1cncfg  45835  expcnfg  45837  fprodabs2  45841  climmulf  45850  climexp  45851  climsuse  45854  climrecf  45855  climinff  45857  climaddf  45861  mullimc  45862  idlimc  45872  limcperiod  45874  neglimc  45891  addlimc  45892  0ellimcdiv  45893  fnlimfv  45907  climreclf  45908  fnlimcnv  45911  fnlimfvre  45918  fnlimfvre2  45921  fnlimf  45922  fnlimabslt  45923  climfveqf  45924  climmptf  45925  climeldmeqf  45927  limsupref  45929  limsupbnd1f  45930  climbddf  45931  climeqf  45932  limsuppnfd  45946  climinf2  45951  limsuppnf  45955  limsupubuz  45957  climinfmpt  45959  limsupmnf  45965  limsupequz  45967  limsupre2  45969  limsupmnfuz  45971  limsupre3  45977  limsupre3uz  45980  limsupreuz  45981  climuz  45988  lmbr3  45991  limsupgt  46022  liminfvalxr  46027  liminfreuz  46047  liminflt  46049  xlimpnfxnegmnf  46058  liminfpnfuz  46060  xlimmnf  46085  xlimpnf  46086  dfxlim2  46092  xlimpnfxnegmnf2  46102  cncfshift  46118  icccncfext  46131  cncficcgt0  46132  cncfiooicclem1  46137  dvnmul  46187  dvnprodlem1  46190  itgsubsticclem  46219  stoweidlem3  46247  stoweidlem23  46267  stoweidlem26  46270  stoweidlem28  46272  stoweidlem29  46273  stoweidlem31  46275  stoweidlem34  46278  stoweidlem36  46280  stoweidlem42  46286  stoweidlem48  46292  stoweidlem51  46295  stoweidlem52  46296  stoweidlem59  46303  wallispilem5  46313  stirlinglem4  46321  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  fourierdlem20  46371  fourierdlem31  46382  fourierdlem79  46429  fourierdlem89  46439  fourierdlem91  46441  fourierdlem112  46462  fourierdlem115  46465  fourierd  46466  fourierclimd  46467  etransclem2  46480  etransclem48  46526  sge0revalmpt  46622  sge0fsummpt  46634  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0xadd  46679  sge0fsummptf  46680  sge0gtfsumgt  46687  iundjiun  46704  meadjiun  46710  voliunsge0lem  46716  meaiunincf  46727  meaiuninc3  46729  omeiunle  46761  omeiunltfirp  46763  ovncvrrp  46808  vonioo  46926  vonicc  46929  vonn0ioo2  46934  vonn0icc2  46936  pimltmnf2f  46941  pimgtpnf2f  46949  pimltpnf2f  46956  pimgtmnf2  46958  pimdecfgtioc  46959  issmff  46978  smfpimltxrmptf  47002  smfpreimagtf  47012  smflim  47021  smfpimgtxr  47024  smfpimgtxrmptf  47028  smfmullem4  47038  smflim2  47050  smfpimcclem  47051  smfpimcc  47052  smfsup  47058  smfsupmpt  47059  smfsupxr  47060  smfinflem  47061  smfinf  47062  smflimsuplem2  47065  smflimsuplem5  47068  smflimsuplem7  47070  smflimsup  47072  smfliminf  47075  fsupdm  47086  smfsupdmmbllem  47088  finfdm  47090  smfinfdmmbllem  47092  nfafv  47382  nfsetrecs  49931  setrec2fun  49937