Theorem nffv 6540

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 6225	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2947	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5003	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiota 6185	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2945	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2931   class class class wbr 4956  ℩cio 6179  ‘cfv 6217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-iota 6181  df-fv 6225

This theorem is referenced by:  nffvmpt1  6541  nffvd  6542  fvelimad  6592  dffn5f  6596  fvmptss  6637  fvmptex  6639  fvmptf  6646  fvmptnf  6647  eqfnfv2f  6662  ralrnmpt  6716  ffnfvf  6737  funiunfvf  6864  dff13f  6870  nfiso  6929  nfwrecs  7791  nfrdg  7893  rdgsucmptf  7907  rdgsucmptnf  7908  frsucmpt  7916  frsucmptn  7917  rankidb  9064  rankval4  9131  dfac8clem  9293  cardaleph  9350  hsmexlem2  9684  axcc2  9694  uniimadomf  9802  nfseq  13217  seqof2  13266  rlim2  14675  nfsum1  14868  nfsum  14869  sumeq2ii  14871  fsumrelem  14983  o1fsum  14989  nfcprod1  15085  nfcprod  15086  fprodefsum  15269  prdsbas3  16571  prdsdsval2  16574  yonedalem4b  17343  gsum2d2lem  18801  coe1fzgsumdlem  20140  evl1gsumdlem  20189  ptcldmpt  21894  ptcnp  21902  cnmpt11  21943  cnmpt21  21951  cnmptk2  21966  prdsdsf  22648  prdsxmet  22650  ovolfiniun  23773  ovoliunlem3  23776  ovoliun  23777  ovoliun2  23778  ovoliunnul  23779  volfiniun  23819  voliun  23826  mbfsup  23936  mbflim  23940  itg2splitlem  24020  itg2split  24021  itg2cnlem1  24033  isibl2  24038  nfitg1  24045  nfitg  24046  cbvitg  24047  itgabs  24106  dvlipcn  24262  lhop2  24283  dvfsumabs  24291  dvfsumrlim  24299  itgparts  24315  itgsubstlem  24316  ulmss  24656  itgulm2  24668  lgamgulmlem2  25277  lgamgulmlem6  25281  lgamgulm2  25283  lgseisenlem2  25622  dchrisumlem3  25737  cnlnadjlem5  29527  dfimafnf  30044  esumfzf  30901  voliune  31061  volfiniune  31062  bnj1534  31697  bnj1542  31701  bnj958  31784  bnj1000  31785  bnj1446  31887  bnj1447  31888  bnj1448  31889  bnj1466  31895  bnj1467  31896  bnj1519  31907  bnj1520  31908  bnj1529  31912  cvmcov  32074  trpredlem1  32620  trpredrec  32631  sltval2  32717  rdgssun  34136  exrecfnlem  34137  finxpreclem2  34148  finxpreclem6  34154  poimirlem23  34392  poimirlem27  34396  itgabsnc  34438  riotaocN  35826  cdleme32d  37061  cdleme32f  37063  ltrniotaval  37198  cdlemksv2  37464  cdlemkuv2  37484  cdlemk36  37530  cdlemk38  37532  cdlemk19x  37560  cdlemk11t  37563  mzpsubst  38780  aomclem8  39097  binomcxplemdvbinom  40175  binomcxplemdvsum  40177  binomcxplemnotnn0  40178  evth2f  40763  fvelrnbf  40766  evthf  40775  rfcnpre3  40781  rfcnpre4  40782  rfcnnnub  40784  refsum2cnlem1  40785  dffo3f  40931  allbutfiinf  41190  monoordxr  41255  monoord2xr  41257  fmul01  41357  fmuldfeqlem1  41359  fmuldfeq  41360  fmul01lt1lem1  41361  fmul01lt1lem2  41362  fmul01lt1  41363  cncfmptss  41364  mulc1cncfg  41366  expcnfg  41368  fprodabs2  41372  climmulf  41381  climexp  41382  climsuse  41385  climrecf  41386  climinff  41388  climaddf  41392  mullimc  41393  idlimc  41403  limcperiod  41405  neglimc  41424  addlimc  41425  0ellimcdiv  41426  fnlimfv  41440  climreclf  41441  fnlimcnv  41444  fnlimfvre  41451  fnlimfvre2  41454  fnlimf  41455  fnlimabslt  41456  climfveqf  41457  climmptf  41458  climeldmeqf  41460  limsupref  41462  limsupbnd1f  41463  climbddf  41464  climeqf  41465  limsuppnfd  41479  climinf2  41484  limsuppnf  41488  limsupubuz  41490  climinfmpt  41492  limsupmnf  41498  limsupequz  41500  limsupre2  41502  limsupmnfuz  41504  limsupre3  41510  limsupre3uz  41513  limsupreuz  41514  climuz  41521  lmbr3  41524  limsupgt  41555  liminfvalxr  41560  liminfreuz  41580  liminflt  41582  xlimpnfxnegmnf  41591  liminfpnfuz  41593  xlimmnf  41618  xlimpnf  41619  dfxlim2  41625  xlimpnfxnegmnf2  41635  cncfshift  41652  icccncfext  41665  cncficcgt0  41666  cncfiooicclem1  41671  dvnmul  41723  dvnprodlem1  41726  itgsubsticclem  41755  stoweidlem3  41784  stoweidlem23  41804  stoweidlem26  41807  stoweidlem28  41809  stoweidlem29  41810  stoweidlem31  41812  stoweidlem34  41815  stoweidlem36  41817  stoweidlem42  41823  stoweidlem48  41829  stoweidlem51  41832  stoweidlem52  41833  stoweidlem59  41840  wallispilem5  41850  stirlinglem4  41858  stirlinglem11  41865  stirlinglem12  41866  stirlinglem13  41867  stirlinglem14  41868  stirlinglem15  41869  fourierdlem20  41908  fourierdlem31  41919  fourierdlem79  41966  fourierdlem89  41976  fourierdlem91  41978  fourierdlem112  41999  fourierdlem115  42002  fourierd  42003  fourierclimd  42004  etransclem2  42017  etransclem48  42063  sge0revalmpt  42156  sge0fsummpt  42168  sge0iunmptlemfi  42191  sge0iunmptlemre  42193  sge0iunmpt  42196  sge0xadd  42213  sge0fsummptf  42214  sge0gtfsumgt  42221  iundjiun  42238  meadjiun  42244  voliunsge0lem  42250  meaiunincf  42261  meaiuninc3  42263  omeiunle  42295  omeiunltfirp  42297  ovncvrrp  42342  vonioo  42460  vonicc  42463  vonn0ioo2  42468  vonn0icc2  42470  pimltmnf2  42475  pimgtpnf2  42481  pimltpnf2  42487  pimgtmnf2  42488  pimdecfgtioc  42489  issmff  42507  smfpimltxrmpt  42531  smfpreimagtf  42540  smflim  42549  smfpimgtxr  42552  smfpimgtxrmpt  42556  smfmullem4  42565  smflim2  42576  smfpimcclem  42577  smfpimcc  42578  smfsup  42584  smfsupmpt  42585  smfsupxr  42586  smfinflem  42587  smfinf  42588  smfinfmpt  42589  smflimsuplem2  42591  smflimsuplem5  42594  smflimsuplem7  42596  smflimsup  42598  smfliminf  42601  nfafv  42805  nfsetrecs  44223  setrec2fun  44229