Theorem nffv 6901

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

Syntax hints:  Ⅎwnfc 2883   class class class wbr 5148  ℩cio 6493  ‘cfv 6543

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551

This theorem is referenced by:  nffvmpt1  6902  nffvd  6903  fvelimad  6959  dffn5f  6963  fvmptss  7010  fvmptex  7012  fvmptf  7019  fvmptnf  7020  eqfnfv2f  7036  ralrnmptw  7095  ralrnmpt  7097  ffnfvf  7118  funiunfvf  7247  dff13f  7254  nfiso  7318  nfwrecsOLD  8301  nfrdg  8413  rdgsucmptf  8427  rdgsucmptnf  8428  frsucmpt  8437  frsucmptn  8438  ttrclselem1  9719  ttrclselem2  9720  rankidb  9794  rankval4  9861  dfac8clem  10026  cardaleph  10083  hsmexlem2  10421  axcc2  10431  uniimadomf  10539  nfseq  13975  seqof2  14025  rlim2  15439  nfsum1  15635  nfsum  15636  sumeq2ii  15638  fsumrelem  15752  o1fsum  15758  nfcprod1  15853  nfcprod  15854  fprodefsum  16037  prdsbas3  17426  prdsdsval2  17429  yonedalem4b  18228  gsum2d2lem  19840  coe1fzgsumdlem  21824  evl1gsumdlem  21874  ptcldmpt  23117  ptcnp  23125  cnmpt11  23166  cnmpt21  23174  cnmptk2  23189  prdsdsf  23872  prdsxmet  23874  ovolfiniun  25017  ovoliunlem3  25020  ovoliun  25021  ovoliun2  25022  ovoliunnul  25023  volfiniun  25063  voliun  25070  mbfsup  25180  mbflim  25184  itg2splitlem  25265  itg2split  25266  itg2cnlem1  25278  isibl2  25283  nfitg1  25290  nfitg  25291  cbvitg  25292  itgabs  25351  dvlipcn  25510  lhop2  25531  dvfsumabs  25539  dvfsumrlim  25547  itgparts  25563  itgsubstlem  25564  ulmss  25908  itgulm2  25920  lgamgulmlem2  26531  lgamgulmlem6  26535  lgamgulm2  26537  lgseisenlem2  26876  dchrisumlem3  26991  sltval2  27156  cnlnadjlem5  31319  dfimafnf  31855  2ndresdju  31869  esumfzf  33062  voliune  33222  volfiniune  33223  bnj1534  33859  bnj1542  33863  bnj958  33946  bnj1000  33947  bnj1446  34051  bnj1447  34052  bnj1448  34053  bnj1466  34059  bnj1467  34060  bnj1519  34071  bnj1520  34072  bnj1529  34076  cvmcov  34249  rdgssun  36254  exrecfnlem  36255  finxpreclem2  36266  finxpreclem6  36272  poimirlem23  36506  poimirlem27  36510  itgabsnc  36552  riotaocN  38074  cdleme32d  39310  cdleme32f  39312  ltrniotaval  39447  cdlemksv2  39713  cdlemkuv2  39733  cdlemk36  39779  cdlemk38  39781  cdlemk19x  39809  cdlemk11t  39812  mzpsubst  41476  aomclem8  41793  mnringmulrcld  42977  binomcxplemdvbinom  43102  binomcxplemdvsum  43104  binomcxplemnotnn0  43105  evth2f  43689  fvelrnbf  43692  evthf  43701  rfcnpre3  43707  rfcnpre4  43708  rfcnnnub  43710  refsum2cnlem1  43711  dffo3f  43867  allbutfiinf  44120  monoordxr  44183  monoord2xr  44185  caucvgbf  44190  cvgcaule  44192  fmul01  44286  fmuldfeqlem1  44288  fmuldfeq  44289  fmul01lt1lem1  44290  fmul01lt1lem2  44291  fmul01lt1  44292  cncfmptss  44293  mulc1cncfg  44295  expcnfg  44297  fprodabs2  44301  climmulf  44310  climexp  44311  climsuse  44314  climrecf  44315  climinff  44317  climaddf  44321  mullimc  44322  idlimc  44332  limcperiod  44334  neglimc  44353  addlimc  44354  0ellimcdiv  44355  fnlimfv  44369  climreclf  44370  fnlimcnv  44373  fnlimfvre  44380  fnlimfvre2  44383  fnlimf  44384  fnlimabslt  44385  climfveqf  44386  climmptf  44387  climeldmeqf  44389  limsupref  44391  limsupbnd1f  44392  climbddf  44393  climeqf  44394  limsuppnfd  44408  climinf2  44413  limsuppnf  44417  limsupubuz  44419  climinfmpt  44421  limsupmnf  44427  limsupequz  44429  limsupre2  44431  limsupmnfuz  44433  limsupre3  44439  limsupre3uz  44442  limsupreuz  44443  climuz  44450  lmbr3  44453  limsupgt  44484  liminfvalxr  44489  liminfreuz  44509  liminflt  44511  xlimpnfxnegmnf  44520  liminfpnfuz  44522  xlimmnf  44547  xlimpnf  44548  dfxlim2  44554  xlimpnfxnegmnf2  44564  cncfshift  44580  icccncfext  44593  cncficcgt0  44594  cncfiooicclem1  44599  dvnmul  44649  dvnprodlem1  44652  itgsubsticclem  44681  stoweidlem3  44709  stoweidlem23  44729  stoweidlem26  44732  stoweidlem28  44734  stoweidlem29  44735  stoweidlem31  44737  stoweidlem34  44740  stoweidlem36  44742  stoweidlem42  44748  stoweidlem48  44754  stoweidlem51  44757  stoweidlem52  44758  stoweidlem59  44765  wallispilem5  44775  stirlinglem4  44783  stirlinglem11  44790  stirlinglem12  44791  stirlinglem13  44792  stirlinglem14  44793  stirlinglem15  44794  fourierdlem20  44833  fourierdlem31  44844  fourierdlem79  44891  fourierdlem89  44901  fourierdlem91  44903  fourierdlem112  44924  fourierdlem115  44927  fourierd  44928  fourierclimd  44929  etransclem2  44942  etransclem48  44988  sge0revalmpt  45084  sge0fsummpt  45096  sge0iunmptlemfi  45119  sge0iunmptlemre  45121  sge0iunmpt  45124  sge0xadd  45141  sge0fsummptf  45142  sge0gtfsumgt  45149  iundjiun  45166  meadjiun  45172  voliunsge0lem  45178  meaiunincf  45189  meaiuninc3  45191  omeiunle  45223  omeiunltfirp  45225  ovncvrrp  45270  vonioo  45388  vonicc  45391  vonn0ioo2  45396  vonn0icc2  45398  pimltmnf2f  45403  pimgtpnf2f  45411  pimltpnf2f  45418  pimgtmnf2  45420  pimdecfgtioc  45421  issmff  45440  smfpimltxrmptf  45464  smfpreimagtf  45474  smflim  45483  smfpimgtxr  45486  smfpimgtxrmptf  45490  smfmullem4  45500  smflim2  45512  smfpimcclem  45513  smfpimcc  45514  smfsup  45520  smfsupmpt  45521  smfsupxr  45522  smfinflem  45523  smfinf  45524  smfinfmpt  45525  smflimsuplem2  45527  smflimsuplem5  45530  smflimsuplem7  45532  smflimsup  45534  smfliminf  45537  fsupdm  45548  smfsupdmmbllem  45550  finfdm  45552  smfinfdmmbllem  45554  nfafv  45834  nfsetrecs  47721  setrec2fun  47727