Theorem nffv 6916

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 6569	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2905	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5190	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6518	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2903	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2890   class class class wbr 5143  ℩cio 6512  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569

This theorem is referenced by:  nffvmpt1  6917  nffvd  6918  fvelimad  6976  dffn5f  6980  fvmptss  7028  fvmptex  7030  fvmptf  7037  fvmptnf  7038  eqfnfv2f  7055  ralrnmptw  7114  ralrnmpt  7116  dffo3f  7126  ffnfvf  7140  funiunfvf  7269  dff13f  7276  nfiso  7342  nfwrecsOLD  8342  nfrdg  8454  rdgsucmptf  8468  rdgsucmptnf  8469  frsucmpt  8478  frsucmptn  8479  ttrclselem1  9765  ttrclselem2  9766  rankidb  9840  rankval4  9907  dfac8clem  10072  cardaleph  10129  hsmexlem2  10467  axcc2  10477  uniimadomf  10585  nfseq  14052  seqof2  14101  rlim2  15532  nfsum1  15726  nfsum  15727  sumeq2ii  15729  fsumrelem  15843  o1fsum  15849  nfcprod1  15944  nfcprod  15945  fprodefsum  16131  prdsbas3  17526  prdsdsval2  17529  yonedalem4b  18321  gsum2d2lem  19991  coe1fzgsumdlem  22307  evl1gsumdlem  22360  ptcldmpt  23622  ptcnp  23630  cnmpt11  23671  cnmpt21  23679  cnmptk2  23694  prdsdsf  24377  prdsxmet  24379  ovolfiniun  25536  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  ovoliunnul  25542  volfiniun  25582  voliun  25589  mbfsup  25699  mbflim  25703  itg2splitlem  25783  itg2split  25784  itg2cnlem1  25796  isibl2  25801  nfitg1  25809  nfitg  25810  cbvitg  25811  itgabs  25870  dvlipcn  26033  lhop2  26054  dvfsumabs  26063  dvfsumrlim  26072  itgparts  26088  itgsubstlem  26089  ulmss  26440  itgulm2  26452  lgamgulmlem2  27073  lgamgulmlem6  27077  lgamgulm2  27079  lgseisenlem2  27420  dchrisumlem3  27535  sltval2  27701  nfseqs  28293  cnlnadjlem5  32090  dfimafnf  32646  2ndresdju  32659  esumfzf  34070  voliune  34230  volfiniune  34231  bnj1534  34867  bnj1542  34871  bnj958  34954  bnj1000  34955  bnj1446  35059  bnj1447  35060  bnj1448  35061  bnj1466  35067  bnj1467  35068  bnj1519  35079  bnj1520  35080  bnj1529  35084  cvmcov  35268  rdgssun  37379  exrecfnlem  37380  finxpreclem2  37391  finxpreclem6  37397  poimirlem23  37650  poimirlem27  37654  itgabsnc  37696  riotaocN  39210  cdleme32d  40446  cdleme32f  40448  ltrniotaval  40583  cdlemksv2  40849  cdlemkuv2  40869  cdlemk36  40915  cdlemk38  40917  cdlemk19x  40945  cdlemk11t  40948  evl1gprodd  42118  mzpsubst  42759  aomclem8  43073  mnringmulrcld  44247  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  nfrelp  44970  evth2f  45020  fvelrnbf  45023  evthf  45032  rfcnpre3  45038  rfcnpre4  45039  rfcnnnub  45041  refsum2cnlem1  45042  allbutfiinf  45431  monoordxr  45493  monoord2xr  45495  caucvgbf  45500  cvgcaule  45502  fmul01  45595  fmuldfeqlem1  45597  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  fmul01lt1  45601  cncfmptss  45602  mulc1cncfg  45604  expcnfg  45606  fprodabs2  45610  climmulf  45619  climexp  45620  climsuse  45623  climrecf  45624  climinff  45626  climaddf  45630  mullimc  45631  idlimc  45641  limcperiod  45643  neglimc  45662  addlimc  45663  0ellimcdiv  45664  fnlimfv  45678  climreclf  45679  fnlimcnv  45682  fnlimfvre  45689  fnlimfvre2  45692  fnlimf  45693  fnlimabslt  45694  climfveqf  45695  climmptf  45696  climeldmeqf  45698  limsupref  45700  limsupbnd1f  45701  climbddf  45702  climeqf  45703  limsuppnfd  45717  climinf2  45722  limsuppnf  45726  limsupubuz  45728  climinfmpt  45730  limsupmnf  45736  limsupequz  45738  limsupre2  45740  limsupmnfuz  45742  limsupre3  45748  limsupre3uz  45751  limsupreuz  45752  climuz  45759  lmbr3  45762  limsupgt  45793  liminfvalxr  45798  liminfreuz  45818  liminflt  45820  xlimpnfxnegmnf  45829  liminfpnfuz  45831  xlimmnf  45856  xlimpnf  45857  dfxlim2  45863  xlimpnfxnegmnf2  45873  cncfshift  45889  icccncfext  45902  cncficcgt0  45903  cncfiooicclem1  45908  dvnmul  45958  dvnprodlem1  45961  itgsubsticclem  45990  stoweidlem3  46018  stoweidlem23  46038  stoweidlem26  46041  stoweidlem28  46043  stoweidlem29  46044  stoweidlem31  46046  stoweidlem34  46049  stoweidlem36  46051  stoweidlem42  46057  stoweidlem48  46063  stoweidlem51  46066  stoweidlem52  46067  stoweidlem59  46074  wallispilem5  46084  stirlinglem4  46092  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  fourierdlem20  46142  fourierdlem31  46153  fourierdlem79  46200  fourierdlem89  46210  fourierdlem91  46212  fourierdlem112  46233  fourierdlem115  46236  fourierd  46237  fourierclimd  46238  etransclem2  46251  etransclem48  46297  sge0revalmpt  46393  sge0fsummpt  46405  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0xadd  46450  sge0fsummptf  46451  sge0gtfsumgt  46458  iundjiun  46475  meadjiun  46481  voliunsge0lem  46487  meaiunincf  46498  meaiuninc3  46500  omeiunle  46532  omeiunltfirp  46534  ovncvrrp  46579  vonioo  46697  vonicc  46700  vonn0ioo2  46705  vonn0icc2  46707  pimltmnf2f  46712  pimgtpnf2f  46720  pimltpnf2f  46727  pimgtmnf2  46729  pimdecfgtioc  46730  issmff  46749  smfpimltxrmptf  46773  smfpreimagtf  46783  smflim  46792  smfpimgtxr  46795  smfpimgtxrmptf  46799  smfmullem4  46809  smflim2  46821  smfpimcclem  46822  smfpimcc  46823  smfsup  46829  smfsupmpt  46830  smfsupxr  46831  smfinflem  46832  smfinf  46833  smflimsuplem2  46836  smflimsuplem5  46839  smflimsuplem7  46841  smflimsup  46843  smfliminf  46846  fsupdm  46857  smfsupdmmbllem  46859  finfdm  46861  smfinfdmmbllem  46863  nfafv  47148  nfsetrecs  49205  setrec2fun  49211