Theorem nffv 6727

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

Syntax hints:  Ⅎwnfc 2884   class class class wbr 5053  ℩cio 6336  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-iota 6338  df-fv 6388

This theorem is referenced by:  nffvmpt1  6728  nffvd  6729  fvelimad  6779  dffn5f  6783  fvmptss  6830  fvmptex  6832  fvmptf  6839  fvmptnf  6840  eqfnfv2f  6856  ralrnmptw  6913  ralrnmpt  6915  ffnfvf  6936  funiunfvf  7062  dff13f  7068  nfiso  7131  nfwrecs  8049  nfrdg  8150  rdgsucmptf  8164  rdgsucmptnf  8165  frsucmpt  8173  frsucmptn  8174  trpredlem1  9332  trpredrec  9342  rankidb  9416  rankval4  9483  dfac8clem  9646  cardaleph  9703  hsmexlem2  10041  axcc2  10051  uniimadomf  10159  nfseq  13584  seqof2  13634  rlim2  15057  nfsum1  15253  nfsum  15254  nfsumOLD  15255  sumeq2ii  15257  fsumrelem  15371  o1fsum  15377  nfcprod1  15472  nfcprod  15473  fprodefsum  15656  prdsbas3  16986  prdsdsval2  16989  yonedalem4b  17784  gsum2d2lem  19358  coe1fzgsumdlem  21222  evl1gsumdlem  21272  ptcldmpt  22511  ptcnp  22519  cnmpt11  22560  cnmpt21  22568  cnmptk2  22583  prdsdsf  23265  prdsxmet  23267  ovolfiniun  24398  ovoliunlem3  24401  ovoliun  24402  ovoliun2  24403  ovoliunnul  24404  volfiniun  24444  voliun  24451  mbfsup  24561  mbflim  24565  itg2splitlem  24646  itg2split  24647  itg2cnlem1  24659  isibl2  24664  nfitg1  24671  nfitg  24672  cbvitg  24673  itgabs  24732  dvlipcn  24891  lhop2  24912  dvfsumabs  24920  dvfsumrlim  24928  itgparts  24944  itgsubstlem  24945  ulmss  25289  itgulm2  25301  lgamgulmlem2  25912  lgamgulmlem6  25916  lgamgulm2  25918  lgseisenlem2  26257  dchrisumlem3  26372  cnlnadjlem5  30152  dfimafnf  30690  2ndresdju  30705  esumfzf  31749  voliune  31909  volfiniune  31910  bnj1534  32546  bnj1542  32550  bnj958  32633  bnj1000  32634  bnj1446  32738  bnj1447  32739  bnj1448  32740  bnj1466  32746  bnj1467  32747  bnj1519  32758  bnj1520  32759  bnj1529  32763  cvmcov  32938  sltval2  33596  rdgssun  35286  exrecfnlem  35287  finxpreclem2  35298  finxpreclem6  35304  poimirlem23  35537  poimirlem27  35541  itgabsnc  35583  riotaocN  36960  cdleme32d  38195  cdleme32f  38197  ltrniotaval  38332  cdlemksv2  38598  cdlemkuv2  38618  cdlemk36  38664  cdlemk38  38666  cdlemk19x  38694  cdlemk11t  38697  mzpsubst  40273  aomclem8  40589  mnringmulrcld  41519  binomcxplemdvbinom  41644  binomcxplemdvsum  41646  binomcxplemnotnn0  41647  evth2f  42231  fvelrnbf  42234  evthf  42243  rfcnpre3  42249  rfcnpre4  42250  rfcnnnub  42252  refsum2cnlem1  42253  dffo3f  42390  allbutfiinf  42633  monoordxr  42698  monoord2xr  42700  fmul01  42796  fmuldfeqlem1  42798  fmuldfeq  42799  fmul01lt1lem1  42800  fmul01lt1lem2  42801  fmul01lt1  42802  cncfmptss  42803  mulc1cncfg  42805  expcnfg  42807  fprodabs2  42811  climmulf  42820  climexp  42821  climsuse  42824  climrecf  42825  climinff  42827  climaddf  42831  mullimc  42832  idlimc  42842  limcperiod  42844  neglimc  42863  addlimc  42864  0ellimcdiv  42865  fnlimfv  42879  climreclf  42880  fnlimcnv  42883  fnlimfvre  42890  fnlimfvre2  42893  fnlimf  42894  fnlimabslt  42895  climfveqf  42896  climmptf  42897  climeldmeqf  42899  limsupref  42901  limsupbnd1f  42902  climbddf  42903  climeqf  42904  limsuppnfd  42918  climinf2  42923  limsuppnf  42927  limsupubuz  42929  climinfmpt  42931  limsupmnf  42937  limsupequz  42939  limsupre2  42941  limsupmnfuz  42943  limsupre3  42949  limsupre3uz  42952  limsupreuz  42953  climuz  42960  lmbr3  42963  limsupgt  42994  liminfvalxr  42999  liminfreuz  43019  liminflt  43021  xlimpnfxnegmnf  43030  liminfpnfuz  43032  xlimmnf  43057  xlimpnf  43058  dfxlim2  43064  xlimpnfxnegmnf2  43074  cncfshift  43090  icccncfext  43103  cncficcgt0  43104  cncfiooicclem1  43109  dvnmul  43159  dvnprodlem1  43162  itgsubsticclem  43191  stoweidlem3  43219  stoweidlem23  43239  stoweidlem26  43242  stoweidlem28  43244  stoweidlem29  43245  stoweidlem31  43247  stoweidlem34  43250  stoweidlem36  43252  stoweidlem42  43258  stoweidlem48  43264  stoweidlem51  43267  stoweidlem52  43268  stoweidlem59  43275  wallispilem5  43285  stirlinglem4  43293  stirlinglem11  43300  stirlinglem12  43301  stirlinglem13  43302  stirlinglem14  43303  stirlinglem15  43304  fourierdlem20  43343  fourierdlem31  43354  fourierdlem79  43401  fourierdlem89  43411  fourierdlem91  43413  fourierdlem112  43434  fourierdlem115  43437  fourierd  43438  fourierclimd  43439  etransclem2  43452  etransclem48  43498  sge0revalmpt  43591  sge0fsummpt  43603  sge0iunmptlemfi  43626  sge0iunmptlemre  43628  sge0iunmpt  43631  sge0xadd  43648  sge0fsummptf  43649  sge0gtfsumgt  43656  iundjiun  43673  meadjiun  43679  voliunsge0lem  43685  meaiunincf  43696  meaiuninc3  43698  omeiunle  43730  omeiunltfirp  43732  ovncvrrp  43777  vonioo  43895  vonicc  43898  vonn0ioo2  43903  vonn0icc2  43905  pimltmnf2  43910  pimgtpnf2  43916  pimltpnf2  43922  pimgtmnf2  43923  pimdecfgtioc  43924  issmff  43942  smfpimltxrmpt  43966  smfpreimagtf  43975  smflim  43984  smfpimgtxr  43987  smfpimgtxrmpt  43991  smfmullem4  44000  smflim2  44011  smfpimcclem  44012  smfpimcc  44013  smfsup  44019  smfsupmpt  44020  smfsupxr  44021  smfinflem  44022  smfinf  44023  smfinfmpt  44024  smflimsuplem2  44026  smflimsuplem5  44029  smflimsuplem7  44031  smflimsup  44033  smfliminf  44036  nfafv  44300  nfsetrecs  46063  setrec2fun  46069