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

Syntax hints:  Ⅎwnfc 2887   class class class wbr 5147  ℩cio 6513  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570

This theorem is referenced by:  nffvmpt1  6917  nffvd  6918  fvelimad  6975  dffn5f  6979  fvmptss  7027  fvmptex  7029  fvmptf  7036  fvmptnf  7037  eqfnfv2f  7054  ralrnmptw  7113  ralrnmpt  7115  dffo3f  7125  ffnfvf  7139  funiunfvf  7268  dff13f  7275  nfiso  7341  nfwrecsOLD  8340  nfrdg  8452  rdgsucmptf  8466  rdgsucmptnf  8467  frsucmpt  8476  frsucmptn  8477  ttrclselem1  9762  ttrclselem2  9763  rankidb  9837  rankval4  9904  dfac8clem  10069  cardaleph  10126  hsmexlem2  10464  axcc2  10474  uniimadomf  10582  nfseq  14048  seqof2  14097  rlim2  15528  nfsum1  15722  nfsum  15723  sumeq2ii  15725  fsumrelem  15839  o1fsum  15845  nfcprod1  15940  nfcprod  15941  fprodefsum  16127  prdsbas3  17527  prdsdsval2  17530  yonedalem4b  18332  gsum2d2lem  20005  coe1fzgsumdlem  22322  evl1gsumdlem  22375  ptcldmpt  23637  ptcnp  23645  cnmpt11  23686  cnmpt21  23694  cnmptk2  23709  prdsdsf  24392  prdsxmet  24394  ovolfiniun  25549  ovoliunlem3  25552  ovoliun  25553  ovoliun2  25554  ovoliunnul  25555  volfiniun  25595  voliun  25602  mbfsup  25712  mbflim  25716  itg2splitlem  25797  itg2split  25798  itg2cnlem1  25810  isibl2  25815  nfitg1  25823  nfitg  25824  cbvitg  25825  itgabs  25884  dvlipcn  26047  lhop2  26068  dvfsumabs  26077  dvfsumrlim  26086  itgparts  26102  itgsubstlem  26103  ulmss  26454  itgulm2  26466  lgamgulmlem2  27087  lgamgulmlem6  27091  lgamgulm2  27093  lgseisenlem2  27434  dchrisumlem3  27549  sltval2  27715  nfseqs  28307  cnlnadjlem5  32099  dfimafnf  32652  2ndresdju  32665  esumfzf  34049  voliune  34209  volfiniune  34210  bnj1534  34845  bnj1542  34849  bnj958  34932  bnj1000  34933  bnj1446  35037  bnj1447  35038  bnj1448  35039  bnj1466  35045  bnj1467  35046  bnj1519  35057  bnj1520  35058  bnj1529  35062  cvmcov  35247  rdgssun  37360  exrecfnlem  37361  finxpreclem2  37372  finxpreclem6  37378  poimirlem23  37629  poimirlem27  37633  itgabsnc  37675  riotaocN  39190  cdleme32d  40426  cdleme32f  40428  ltrniotaval  40563  cdlemksv2  40829  cdlemkuv2  40849  cdlemk36  40895  cdlemk38  40897  cdlemk19x  40925  cdlemk11t  40928  evl1gprodd  42098  mzpsubst  42735  aomclem8  43049  mnringmulrcld  44223  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  evth2f  44952  fvelrnbf  44955  evthf  44964  rfcnpre3  44970  rfcnpre4  44971  rfcnnnub  44973  refsum2cnlem1  44974  allbutfiinf  45369  monoordxr  45432  monoord2xr  45434  caucvgbf  45439  cvgcaule  45441  fmul01  45535  fmuldfeqlem1  45537  fmuldfeq  45538  fmul01lt1lem1  45539  fmul01lt1lem2  45540  fmul01lt1  45541  cncfmptss  45542  mulc1cncfg  45544  expcnfg  45546  fprodabs2  45550  climmulf  45559  climexp  45560  climsuse  45563  climrecf  45564  climinff  45566  climaddf  45570  mullimc  45571  idlimc  45581  limcperiod  45583  neglimc  45602  addlimc  45603  0ellimcdiv  45604  fnlimfv  45618  climreclf  45619  fnlimcnv  45622  fnlimfvre  45629  fnlimfvre2  45632  fnlimf  45633  fnlimabslt  45634  climfveqf  45635  climmptf  45636  climeldmeqf  45638  limsupref  45640  limsupbnd1f  45641  climbddf  45642  climeqf  45643  limsuppnfd  45657  climinf2  45662  limsuppnf  45666  limsupubuz  45668  climinfmpt  45670  limsupmnf  45676  limsupequz  45678  limsupre2  45680  limsupmnfuz  45682  limsupre3  45688  limsupre3uz  45691  limsupreuz  45692  climuz  45699  lmbr3  45702  limsupgt  45733  liminfvalxr  45738  liminfreuz  45758  liminflt  45760  xlimpnfxnegmnf  45769  liminfpnfuz  45771  xlimmnf  45796  xlimpnf  45797  dfxlim2  45803  xlimpnfxnegmnf2  45813  cncfshift  45829  icccncfext  45842  cncficcgt0  45843  cncfiooicclem1  45848  dvnmul  45898  dvnprodlem1  45901  itgsubsticclem  45930  stoweidlem3  45958  stoweidlem23  45978  stoweidlem26  45981  stoweidlem28  45983  stoweidlem29  45984  stoweidlem31  45986  stoweidlem34  45989  stoweidlem36  45991  stoweidlem42  45997  stoweidlem48  46003  stoweidlem51  46006  stoweidlem52  46007  stoweidlem59  46014  wallispilem5  46024  stirlinglem4  46032  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  fourierdlem20  46082  fourierdlem31  46093  fourierdlem79  46140  fourierdlem89  46150  fourierdlem91  46152  fourierdlem112  46173  fourierdlem115  46176  fourierd  46177  fourierclimd  46178  etransclem2  46191  etransclem48  46237  sge0revalmpt  46333  sge0fsummpt  46345  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0xadd  46390  sge0fsummptf  46391  sge0gtfsumgt  46398  iundjiun  46415  meadjiun  46421  voliunsge0lem  46427  meaiunincf  46438  meaiuninc3  46440  omeiunle  46472  omeiunltfirp  46474  ovncvrrp  46519  vonioo  46637  vonicc  46640  vonn0ioo2  46645  vonn0icc2  46647  pimltmnf2f  46652  pimgtpnf2f  46660  pimltpnf2f  46667  pimgtmnf2  46669  pimdecfgtioc  46670  issmff  46689  smfpimltxrmptf  46713  smfpreimagtf  46723  smflim  46732  smfpimgtxr  46735  smfpimgtxrmptf  46739  smfmullem4  46749  smflim2  46761  smfpimcclem  46762  smfpimcc  46763  smfsup  46769  smfsupmpt  46770  smfsupxr  46771  smfinflem  46772  smfinf  46773  smflimsuplem2  46776  smflimsuplem5  46779  smflimsuplem7  46781  smflimsup  46783  smfliminf  46786  fsupdm  46797  smfsupdmmbllem  46799  finfdm  46801  smfinfdmmbllem  46803  nfafv  47085  nfsetrecs  48916  setrec2fun  48922