Theorem nffv 6868

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

Syntax hints:  Ⅎwnfc 2876   class class class wbr 5107  ℩cio 6462  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519

This theorem is referenced by:  nffvmpt1  6869  nffvd  6870  fvelimad  6928  dffn5f  6932  fvmptss  6980  fvmptex  6982  fvmptf  6989  fvmptnf  6990  eqfnfv2f  7007  ralrnmptw  7066  ralrnmpt  7068  dffo3f  7078  ffnfvf  7092  funiunfvf  7223  dff13f  7230  nfiso  7297  nfrdg  8382  rdgsucmptf  8396  rdgsucmptnf  8397  frsucmpt  8406  frsucmptn  8407  ttrclselem1  9678  ttrclselem2  9679  rankidb  9753  rankval4  9820  dfac8clem  9985  cardaleph  10042  hsmexlem2  10380  axcc2  10390  uniimadomf  10498  nfseq  13976  seqof2  14025  rlim2  15462  nfsum1  15656  nfsum  15657  sumeq2ii  15659  fsumrelem  15773  o1fsum  15779  nfcprod1  15874  nfcprod  15875  fprodefsum  16061  prdsbas3  17444  prdsdsval2  17447  yonedalem4b  18237  gsum2d2lem  19903  coe1fzgsumdlem  22190  evl1gsumdlem  22243  ptcldmpt  23501  ptcnp  23509  cnmpt11  23550  cnmpt21  23558  cnmptk2  23573  prdsdsf  24255  prdsxmet  24257  ovolfiniun  25402  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  ovoliunnul  25408  volfiniun  25448  voliun  25455  mbfsup  25565  mbflim  25569  itg2splitlem  25649  itg2split  25650  itg2cnlem1  25662  isibl2  25667  nfitg1  25675  nfitg  25676  cbvitg  25677  itgabs  25736  dvlipcn  25899  lhop2  25920  dvfsumabs  25929  dvfsumrlim  25938  itgparts  25954  itgsubstlem  25955  ulmss  26306  itgulm2  26318  lgamgulmlem2  26940  lgamgulmlem6  26944  lgamgulm2  26946  lgseisenlem2  27287  dchrisumlem3  27402  sltval2  27568  nfseqs  28181  cnlnadjlem5  32000  dfimafnf  32560  2ndresdju  32573  esumfzf  34059  voliune  34219  volfiniune  34220  bnj1534  34843  bnj1542  34847  bnj958  34930  bnj1000  34931  bnj1446  35035  bnj1447  35036  bnj1448  35037  bnj1466  35043  bnj1467  35044  bnj1519  35055  bnj1520  35056  bnj1529  35060  onvf1odlem2  35091  cvmcov  35250  rdgssun  37366  exrecfnlem  37367  finxpreclem2  37378  finxpreclem6  37384  poimirlem23  37637  poimirlem27  37641  itgabsnc  37683  riotaocN  39202  cdleme32d  40438  cdleme32f  40440  ltrniotaval  40575  cdlemksv2  40841  cdlemkuv2  40861  cdlemk36  40907  cdlemk38  40909  cdlemk19x  40937  cdlemk11t  40940  evl1gprodd  42105  mzpsubst  42736  aomclem8  43050  mnringmulrcld  44217  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  nfrelp  44939  permaxrep  44996  permaxsep  44997  evth2f  45009  fvelrnbf  45012  evthf  45021  rfcnpre3  45027  rfcnpre4  45028  rfcnnnub  45030  refsum2cnlem1  45031  allbutfiinf  45416  monoordxr  45478  monoord2xr  45480  caucvgbf  45485  cvgcaule  45487  fmul01  45578  fmuldfeqlem1  45580  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  fmul01lt1  45584  cncfmptss  45585  mulc1cncfg  45587  expcnfg  45589  fprodabs2  45593  climmulf  45602  climexp  45603  climsuse  45606  climrecf  45607  climinff  45609  climaddf  45613  mullimc  45614  idlimc  45624  limcperiod  45626  neglimc  45645  addlimc  45646  0ellimcdiv  45647  fnlimfv  45661  climreclf  45662  fnlimcnv  45665  fnlimfvre  45672  fnlimfvre2  45675  fnlimf  45676  fnlimabslt  45677  climfveqf  45678  climmptf  45679  climeldmeqf  45681  limsupref  45683  limsupbnd1f  45684  climbddf  45685  climeqf  45686  limsuppnfd  45700  climinf2  45705  limsuppnf  45709  limsupubuz  45711  climinfmpt  45713  limsupmnf  45719  limsupequz  45721  limsupre2  45723  limsupmnfuz  45725  limsupre3  45731  limsupre3uz  45734  limsupreuz  45735  climuz  45742  lmbr3  45745  limsupgt  45776  liminfvalxr  45781  liminfreuz  45801  liminflt  45803  xlimpnfxnegmnf  45812  liminfpnfuz  45814  xlimmnf  45839  xlimpnf  45840  dfxlim2  45846  xlimpnfxnegmnf2  45856  cncfshift  45872  icccncfext  45885  cncficcgt0  45886  cncfiooicclem1  45891  dvnmul  45941  dvnprodlem1  45944  itgsubsticclem  45973  stoweidlem3  46001  stoweidlem23  46021  stoweidlem26  46024  stoweidlem28  46026  stoweidlem29  46027  stoweidlem31  46029  stoweidlem34  46032  stoweidlem36  46034  stoweidlem42  46040  stoweidlem48  46046  stoweidlem51  46049  stoweidlem52  46050  stoweidlem59  46057  wallispilem5  46067  stirlinglem4  46075  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  fourierdlem20  46125  fourierdlem31  46136  fourierdlem79  46183  fourierdlem89  46193  fourierdlem91  46195  fourierdlem112  46216  fourierdlem115  46219  fourierd  46220  fourierclimd  46221  etransclem2  46234  etransclem48  46280  sge0revalmpt  46376  sge0fsummpt  46388  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0xadd  46433  sge0fsummptf  46434  sge0gtfsumgt  46441  iundjiun  46458  meadjiun  46464  voliunsge0lem  46470  meaiunincf  46481  meaiuninc3  46483  omeiunle  46515  omeiunltfirp  46517  ovncvrrp  46562  vonioo  46680  vonicc  46683  vonn0ioo2  46688  vonn0icc2  46690  pimltmnf2f  46695  pimgtpnf2f  46703  pimltpnf2f  46710  pimgtmnf2  46712  pimdecfgtioc  46713  issmff  46732  smfpimltxrmptf  46756  smfpreimagtf  46766  smflim  46775  smfpimgtxr  46778  smfpimgtxrmptf  46782  smfmullem4  46792  smflim2  46804  smfpimcclem  46805  smfpimcc  46806  smfsup  46812  smfsupmpt  46813  smfsupxr  46814  smfinflem  46815  smfinf  46816  smflimsuplem2  46819  smflimsuplem5  46822  smflimsuplem7  46824  smflimsup  46826  smfliminf  46829  fsupdm  46840  smfsupdmmbllem  46842  finfdm  46844  smfinfdmmbllem  46846  nfafv  47137  nfsetrecs  49675  setrec2fun  49681