Theorem nffv 6845

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 6501	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2899	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5133	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6453	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2897	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2884   class class class wbr 5086  ℩cio 6447  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501

This theorem is referenced by:  nffvmpt1  6846  nffvd  6847  fvelimad  6902  dffn5f  6906  fvmptss  6955  fvmptex  6957  fvmptf  6964  fvmptnf  6965  eqfnfv2f  6982  ralrnmptw  7041  ralrnmpt  7043  dffo3f  7053  ffnfvf  7067  funiunfvf  7198  dff13f  7204  nfiso  7271  nfrdg  8347  rdgsucmptf  8361  rdgsucmptnf  8362  frsucmpt  8371  frsucmptn  8372  ttrclselem1  9640  ttrclselem2  9641  rankidb  9718  rankval4  9785  dfac8clem  9948  cardaleph  10005  hsmexlem2  10343  axcc2  10353  uniimadomf  10461  nfseq  13967  seqof2  14016  rlim2  15452  nfsum1  15646  nfsum  15647  sumeq2ii  15649  fsumrelem  15764  o1fsum  15770  nfcprod1  15867  nfcprod  15868  fprodefsum  16054  prdsbas3  17438  prdsdsval2  17441  yonedalem4b  18236  gsum2d2lem  19942  coe1fzgsumdlem  22281  evl1gsumdlem  22334  ptcldmpt  23592  ptcnp  23600  cnmpt11  23641  cnmpt21  23649  cnmptk2  23664  prdsdsf  24345  prdsxmet  24347  ovolfiniun  25481  ovoliunlem3  25484  ovoliun  25485  ovoliun2  25486  ovoliunnul  25487  volfiniun  25527  voliun  25534  mbfsup  25644  mbflim  25648  itg2splitlem  25728  itg2split  25729  itg2cnlem1  25741  isibl2  25746  nfitg1  25754  nfitg  25755  cbvitg  25756  itgabs  25815  dvlipcn  25974  lhop2  25995  dvfsumabs  26003  dvfsumrlim  26011  itgparts  26027  itgsubstlem  26028  ulmss  26378  itgulm2  26390  lgamgulmlem2  27010  lgamgulmlem6  27014  lgamgulm2  27016  lgseisenlem2  27356  dchrisumlem3  27471  ltsval2  27637  nfseqs  28296  cnlnadjlem5  32160  dfimafnf  32727  2ndresdju  32740  deg1prod  33661  esumfzf  34232  voliune  34392  volfiniune  34393  bnj1534  35014  bnj1542  35018  bnj958  35101  bnj1000  35102  bnj1446  35206  bnj1447  35207  bnj1448  35208  bnj1466  35214  bnj1467  35215  bnj1519  35226  bnj1520  35227  bnj1529  35231  rankval4b  35262  onvf1odlem2  35305  cvmcov  35464  rdgssun  37711  exrecfnlem  37712  finxpreclem2  37723  finxpreclem6  37729  poimirlem23  37981  poimirlem27  37985  itgabsnc  38027  riotaocN  39672  cdleme32d  40907  cdleme32f  40909  ltrniotaval  41044  cdlemksv2  41310  cdlemkuv2  41330  cdlemk36  41376  cdlemk38  41378  cdlemk19x  41406  cdlemk11t  41409  evl1gprodd  42573  mzpsubst  43197  aomclem8  43510  mnringmulrcld  44676  binomcxplemdvbinom  44801  binomcxplemdvsum  44803  binomcxplemnotnn0  44804  nfrelp  45397  permaxrep  45454  permaxsep  45455  evth2f  45467  fvelrnbf  45470  evthf  45479  rfcnpre3  45485  rfcnpre4  45486  rfcnnnub  45488  refsum2cnlem1  45489  allbutfiinf  45869  monoordxr  45931  monoord2xr  45933  caucvgbf  45938  cvgcaule  45940  fmul01  46031  fmuldfeqlem1  46033  fmuldfeq  46034  fmul01lt1lem1  46035  fmul01lt1lem2  46036  fmul01lt1  46037  cncfmptss  46038  mulc1cncfg  46040  expcnfg  46042  fprodabs2  46046  climmulf  46055  climexp  46056  climsuse  46059  climrecf  46060  climinff  46062  climaddf  46066  mullimc  46067  idlimc  46077  limcperiod  46079  neglimc  46096  addlimc  46097  0ellimcdiv  46098  fnlimfv  46112  climreclf  46113  fnlimcnv  46116  fnlimfvre  46123  fnlimfvre2  46126  fnlimf  46127  fnlimabslt  46128  climfveqf  46129  climmptf  46130  climeldmeqf  46132  limsupref  46134  limsupbnd1f  46135  climbddf  46136  climeqf  46137  limsuppnfd  46151  climinf2  46156  limsuppnf  46160  limsupubuz  46162  climinfmpt  46164  limsupmnf  46170  limsupequz  46172  limsupre2  46174  limsupmnfuz  46176  limsupre3  46182  limsupre3uz  46185  limsupreuz  46186  climuz  46193  lmbr3  46196  limsupgt  46227  liminfvalxr  46232  liminfreuz  46252  liminflt  46254  xlimpnfxnegmnf  46263  liminfpnfuz  46265  xlimmnf  46290  xlimpnf  46291  dfxlim2  46297  xlimpnfxnegmnf2  46307  cncfshift  46323  icccncfext  46336  cncficcgt0  46337  cncfiooicclem1  46342  dvnmul  46392  dvnprodlem1  46395  itgsubsticclem  46424  stoweidlem3  46452  stoweidlem23  46472  stoweidlem26  46475  stoweidlem28  46477  stoweidlem29  46478  stoweidlem31  46480  stoweidlem34  46483  stoweidlem36  46485  stoweidlem42  46491  stoweidlem48  46497  stoweidlem51  46500  stoweidlem52  46501  stoweidlem59  46508  wallispilem5  46518  stirlinglem4  46526  stirlinglem11  46533  stirlinglem12  46534  stirlinglem13  46535  stirlinglem14  46536  stirlinglem15  46537  fourierdlem20  46576  fourierdlem31  46587  fourierdlem79  46634  fourierdlem89  46644  fourierdlem91  46646  fourierdlem112  46667  fourierdlem115  46670  fourierd  46671  fourierclimd  46672  etransclem2  46685  etransclem48  46731  sge0revalmpt  46827  sge0fsummpt  46839  sge0iunmptlemfi  46862  sge0iunmptlemre  46864  sge0iunmpt  46867  sge0xadd  46884  sge0fsummptf  46885  sge0gtfsumgt  46892  iundjiun  46909  meadjiun  46915  voliunsge0lem  46921  meaiunincf  46932  meaiuninc3  46934  omeiunle  46966  omeiunltfirp  46968  ovncvrrp  47013  vonioo  47131  vonicc  47134  vonn0ioo2  47139  vonn0icc2  47141  pimltmnf2f  47146  pimgtpnf2f  47154  pimltpnf2f  47161  pimgtmnf2  47163  pimdecfgtioc  47164  issmff  47183  smfpimltxrmptf  47207  smfpreimagtf  47217  smflim  47226  smfpimgtxr  47229  smfpimgtxrmptf  47233  smfmullem4  47243  smflim2  47255  smfpimcclem  47256  smfpimcc  47257  smfsup  47263  smfsupmpt  47264  smfsupxr  47265  smfinflem  47266  smfinf  47267  smflimsuplem2  47270  smflimsuplem5  47273  smflimsuplem7  47275  smflimsup  47277  smfliminf  47280  fsupdm  47291  smfsupdmmbllem  47293  finfdm  47295  smfinfdmmbllem  47297  nfafv  47599  nfsetrecs  50176  setrec2fun  50182