Theorem nffv 6903

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 6554	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2892	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5192	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6502	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2890	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2876   class class class wbr 5145  ℩cio 6496  ‘cfv 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-iota 6498  df-fv 6554

This theorem is referenced by:  nffvmpt1  6904  nffvd  6905  fvelimad  6962  dffn5f  6966  fvmptss  7013  fvmptex  7015  fvmptf  7022  fvmptnf  7023  eqfnfv2f  7040  ralrnmptw  7100  ralrnmpt  7102  dffo3f  7112  ffnfvf  7126  funiunfvf  7256  dff13f  7263  nfiso  7326  nfwrecsOLD  8324  nfrdg  8436  rdgsucmptf  8450  rdgsucmptnf  8451  frsucmpt  8460  frsucmptn  8461  ttrclselem1  9761  ttrclselem2  9762  rankidb  9836  rankval4  9903  dfac8clem  10068  cardaleph  10125  hsmexlem2  10461  axcc2  10471  uniimadomf  10579  nfseq  14025  seqof2  14074  rlim2  15493  nfsum1  15689  nfsum  15690  sumeq2ii  15692  fsumrelem  15806  o1fsum  15812  nfcprod1  15907  nfcprod  15908  fprodefsum  16092  prdsbas3  17491  prdsdsval2  17494  yonedalem4b  18296  gsum2d2lem  19967  coe1fzgsumdlem  22291  evl1gsumdlem  22344  ptcldmpt  23606  ptcnp  23614  cnmpt11  23655  cnmpt21  23663  cnmptk2  23678  prdsdsf  24361  prdsxmet  24363  ovolfiniun  25518  ovoliunlem3  25521  ovoliun  25522  ovoliun2  25523  ovoliunnul  25524  volfiniun  25564  voliun  25571  mbfsup  25681  mbflim  25685  itg2splitlem  25766  itg2split  25767  itg2cnlem1  25779  isibl2  25784  nfitg1  25791  nfitg  25792  cbvitg  25793  itgabs  25852  dvlipcn  26015  lhop2  26036  dvfsumabs  26045  dvfsumrlim  26054  itgparts  26070  itgsubstlem  26071  ulmss  26423  itgulm2  26435  lgamgulmlem2  27055  lgamgulmlem6  27059  lgamgulm2  27061  lgseisenlem2  27402  dchrisumlem3  27517  sltval2  27683  nfseqs  28258  cnlnadjlem5  32001  dfimafnf  32553  2ndresdju  32566  esumfzf  33915  voliune  34075  volfiniune  34076  bnj1534  34711  bnj1542  34715  bnj958  34798  bnj1000  34799  bnj1446  34903  bnj1447  34904  bnj1448  34905  bnj1466  34911  bnj1467  34912  bnj1519  34923  bnj1520  34924  bnj1529  34928  cvmcov  35104  rdgssun  37098  exrecfnlem  37099  finxpreclem2  37110  finxpreclem6  37116  poimirlem23  37357  poimirlem27  37361  itgabsnc  37403  riotaocN  38920  cdleme32d  40156  cdleme32f  40158  ltrniotaval  40293  cdlemksv2  40559  cdlemkuv2  40579  cdlemk36  40625  cdlemk38  40627  cdlemk19x  40655  cdlemk11t  40658  evl1gprodd  41829  mzpsubst  42442  aomclem8  42759  mnringmulrcld  43939  binomcxplemdvbinom  44064  binomcxplemdvsum  44066  binomcxplemnotnn0  44067  evth2f  44651  fvelrnbf  44654  evthf  44663  rfcnpre3  44669  rfcnpre4  44670  rfcnnnub  44672  refsum2cnlem1  44673  allbutfiinf  45071  monoordxr  45134  monoord2xr  45136  caucvgbf  45141  cvgcaule  45143  fmul01  45237  fmuldfeqlem1  45239  fmuldfeq  45240  fmul01lt1lem1  45241  fmul01lt1lem2  45242  fmul01lt1  45243  cncfmptss  45244  mulc1cncfg  45246  expcnfg  45248  fprodabs2  45252  climmulf  45261  climexp  45262  climsuse  45265  climrecf  45266  climinff  45268  climaddf  45272  mullimc  45273  idlimc  45283  limcperiod  45285  neglimc  45304  addlimc  45305  0ellimcdiv  45306  fnlimfv  45320  climreclf  45321  fnlimcnv  45324  fnlimfvre  45331  fnlimfvre2  45334  fnlimf  45335  fnlimabslt  45336  climfveqf  45337  climmptf  45338  climeldmeqf  45340  limsupref  45342  limsupbnd1f  45343  climbddf  45344  climeqf  45345  limsuppnfd  45359  climinf2  45364  limsuppnf  45368  limsupubuz  45370  climinfmpt  45372  limsupmnf  45378  limsupequz  45380  limsupre2  45382  limsupmnfuz  45384  limsupre3  45390  limsupre3uz  45393  limsupreuz  45394  climuz  45401  lmbr3  45404  limsupgt  45435  liminfvalxr  45440  liminfreuz  45460  liminflt  45462  xlimpnfxnegmnf  45471  liminfpnfuz  45473  xlimmnf  45498  xlimpnf  45499  dfxlim2  45505  xlimpnfxnegmnf2  45515  cncfshift  45531  icccncfext  45544  cncficcgt0  45545  cncfiooicclem1  45550  dvnmul  45600  dvnprodlem1  45603  itgsubsticclem  45632  stoweidlem3  45660  stoweidlem23  45680  stoweidlem26  45683  stoweidlem28  45685  stoweidlem29  45686  stoweidlem31  45688  stoweidlem34  45691  stoweidlem36  45693  stoweidlem42  45699  stoweidlem48  45705  stoweidlem51  45708  stoweidlem52  45709  stoweidlem59  45716  wallispilem5  45726  stirlinglem4  45734  stirlinglem11  45741  stirlinglem12  45742  stirlinglem13  45743  stirlinglem14  45744  stirlinglem15  45745  fourierdlem20  45784  fourierdlem31  45795  fourierdlem79  45842  fourierdlem89  45852  fourierdlem91  45854  fourierdlem112  45875  fourierdlem115  45878  fourierd  45879  fourierclimd  45880  etransclem2  45893  etransclem48  45939  sge0revalmpt  46035  sge0fsummpt  46047  sge0iunmptlemfi  46070  sge0iunmptlemre  46072  sge0iunmpt  46075  sge0xadd  46092  sge0fsummptf  46093  sge0gtfsumgt  46100  iundjiun  46117  meadjiun  46123  voliunsge0lem  46129  meaiunincf  46140  meaiuninc3  46142  omeiunle  46174  omeiunltfirp  46176  ovncvrrp  46221  vonioo  46339  vonicc  46342  vonn0ioo2  46347  vonn0icc2  46349  pimltmnf2f  46354  pimgtpnf2f  46362  pimltpnf2f  46369  pimgtmnf2  46371  pimdecfgtioc  46372  issmff  46391  smfpimltxrmptf  46415  smfpreimagtf  46425  smflim  46434  smfpimgtxr  46437  smfpimgtxrmptf  46441  smfmullem4  46451  smflim2  46463  smfpimcclem  46464  smfpimcc  46465  smfsup  46471  smfsupmpt  46472  smfsupxr  46473  smfinflem  46474  smfinf  46475  smfinfmpt  46476  smflimsuplem2  46478  smflimsuplem5  46481  smflimsuplem7  46483  smflimsup  46485  smfliminf  46488  fsupdm  46499  smfsupdmmbllem  46501  finfdm  46503  smfinfdmmbllem  46505  nfafv  46785  nfsetrecs  48468  setrec2fun  48474