Theorem nffv 6852

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 6508	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2899	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5147	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6460	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2897	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2884   class class class wbr 5100  ℩cio 6454  ‘cfv 6500

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508

This theorem is referenced by:  nffvmpt1  6853  nffvd  6854  fvelimad  6909  dffn5f  6913  fvmptss  6962  fvmptex  6964  fvmptf  6971  fvmptnf  6972  eqfnfv2f  6989  ralrnmptw  7048  ralrnmpt  7050  dffo3f  7060  ffnfvf  7074  funiunfvf  7205  dff13f  7211  nfiso  7278  nfrdg  8355  rdgsucmptf  8369  rdgsucmptnf  8370  frsucmpt  8379  frsucmptn  8380  ttrclselem1  9646  ttrclselem2  9647  rankidb  9724  rankval4  9791  dfac8clem  9954  cardaleph  10011  hsmexlem2  10349  axcc2  10359  uniimadomf  10467  nfseq  13946  seqof2  13995  rlim2  15431  nfsum1  15625  nfsum  15626  sumeq2ii  15628  fsumrelem  15742  o1fsum  15748  nfcprod1  15843  nfcprod  15844  fprodefsum  16030  prdsbas3  17413  prdsdsval2  17416  yonedalem4b  18211  gsum2d2lem  19914  coe1fzgsumdlem  22259  evl1gsumdlem  22312  ptcldmpt  23570  ptcnp  23578  cnmpt11  23619  cnmpt21  23627  cnmptk2  23642  prdsdsf  24323  prdsxmet  24325  ovolfiniun  25470  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  ovoliunnul  25476  volfiniun  25516  voliun  25523  mbfsup  25633  mbflim  25637  itg2splitlem  25717  itg2split  25718  itg2cnlem1  25730  isibl2  25735  nfitg1  25743  nfitg  25744  cbvitg  25745  itgabs  25804  dvlipcn  25967  lhop2  25988  dvfsumabs  25997  dvfsumrlim  26006  itgparts  26022  itgsubstlem  26023  ulmss  26374  itgulm2  26386  lgamgulmlem2  27008  lgamgulmlem6  27012  lgamgulm2  27014  lgseisenlem2  27355  dchrisumlem3  27470  ltsval2  27636  nfseqs  28295  cnlnadjlem5  32159  dfimafnf  32726  2ndresdju  32739  deg1prod  33676  esumfzf  34247  voliune  34407  volfiniune  34408  bnj1534  35029  bnj1542  35033  bnj958  35116  bnj1000  35117  bnj1446  35221  bnj1447  35222  bnj1448  35223  bnj1466  35229  bnj1467  35230  bnj1519  35241  bnj1520  35242  bnj1529  35246  rankval4b  35277  onvf1odlem2  35320  cvmcov  35479  rdgssun  37633  exrecfnlem  37634  finxpreclem2  37645  finxpreclem6  37651  poimirlem23  37894  poimirlem27  37898  itgabsnc  37940  riotaocN  39585  cdleme32d  40820  cdleme32f  40822  ltrniotaval  40957  cdlemksv2  41223  cdlemkuv2  41243  cdlemk36  41289  cdlemk38  41291  cdlemk19x  41319  cdlemk11t  41322  evl1gprodd  42487  mzpsubst  43105  aomclem8  43418  mnringmulrcld  44584  binomcxplemdvbinom  44709  binomcxplemdvsum  44711  binomcxplemnotnn0  44712  nfrelp  45305  permaxrep  45362  permaxsep  45363  evth2f  45375  fvelrnbf  45378  evthf  45387  rfcnpre3  45393  rfcnpre4  45394  rfcnnnub  45396  refsum2cnlem1  45397  allbutfiinf  45778  monoordxr  45840  monoord2xr  45842  caucvgbf  45847  cvgcaule  45849  fmul01  45940  fmuldfeqlem1  45942  fmuldfeq  45943  fmul01lt1lem1  45944  fmul01lt1lem2  45945  fmul01lt1  45946  cncfmptss  45947  mulc1cncfg  45949  expcnfg  45951  fprodabs2  45955  climmulf  45964  climexp  45965  climsuse  45968  climrecf  45969  climinff  45971  climaddf  45975  mullimc  45976  idlimc  45986  limcperiod  45988  neglimc  46005  addlimc  46006  0ellimcdiv  46007  fnlimfv  46021  climreclf  46022  fnlimcnv  46025  fnlimfvre  46032  fnlimfvre2  46035  fnlimf  46036  fnlimabslt  46037  climfveqf  46038  climmptf  46039  climeldmeqf  46041  limsupref  46043  limsupbnd1f  46044  climbddf  46045  climeqf  46046  limsuppnfd  46060  climinf2  46065  limsuppnf  46069  limsupubuz  46071  climinfmpt  46073  limsupmnf  46079  limsupequz  46081  limsupre2  46083  limsupmnfuz  46085  limsupre3  46091  limsupre3uz  46094  limsupreuz  46095  climuz  46102  lmbr3  46105  limsupgt  46136  liminfvalxr  46141  liminfreuz  46161  liminflt  46163  xlimpnfxnegmnf  46172  liminfpnfuz  46174  xlimmnf  46199  xlimpnf  46200  dfxlim2  46206  xlimpnfxnegmnf2  46216  cncfshift  46232  icccncfext  46245  cncficcgt0  46246  cncfiooicclem1  46251  dvnmul  46301  dvnprodlem1  46304  itgsubsticclem  46333  stoweidlem3  46361  stoweidlem23  46381  stoweidlem26  46384  stoweidlem28  46386  stoweidlem29  46387  stoweidlem31  46389  stoweidlem34  46392  stoweidlem36  46394  stoweidlem42  46400  stoweidlem48  46406  stoweidlem51  46409  stoweidlem52  46410  stoweidlem59  46417  wallispilem5  46427  stirlinglem4  46435  stirlinglem11  46442  stirlinglem12  46443  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  fourierdlem20  46485  fourierdlem31  46496  fourierdlem79  46543  fourierdlem89  46553  fourierdlem91  46555  fourierdlem112  46576  fourierdlem115  46579  fourierd  46580  fourierclimd  46581  etransclem2  46594  etransclem48  46640  sge0revalmpt  46736  sge0fsummpt  46748  sge0iunmptlemfi  46771  sge0iunmptlemre  46773  sge0iunmpt  46776  sge0xadd  46793  sge0fsummptf  46794  sge0gtfsumgt  46801  iundjiun  46818  meadjiun  46824  voliunsge0lem  46830  meaiunincf  46841  meaiuninc3  46843  omeiunle  46875  omeiunltfirp  46877  ovncvrrp  46922  vonioo  47040  vonicc  47043  vonn0ioo2  47048  vonn0icc2  47050  pimltmnf2f  47055  pimgtpnf2f  47063  pimltpnf2f  47070  pimgtmnf2  47072  pimdecfgtioc  47073  issmff  47092  smfpimltxrmptf  47116  smfpreimagtf  47126  smflim  47135  smfpimgtxr  47138  smfpimgtxrmptf  47142  smfmullem4  47152  smflim2  47164  smfpimcclem  47165  smfpimcc  47166  smfsup  47172  smfsupmpt  47173  smfsupxr  47174  smfinflem  47175  smfinf  47176  smflimsuplem2  47179  smflimsuplem5  47182  smflimsuplem7  47184  smflimsup  47186  smfliminf  47189  fsupdm  47200  smfsupdmmbllem  47202  finfdm  47204  smfinfdmmbllem  47206  nfafv  47496  nfsetrecs  50045  setrec2fun  50051