Theorem nffv 6850

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

Syntax hints:  Ⅎwnfc 2876   class class class wbr 5102  ℩cio 6450  ‘cfv 6499

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507

This theorem is referenced by:  nffvmpt1  6851  nffvd  6852  fvelimad  6910  dffn5f  6914  fvmptss  6962  fvmptex  6964  fvmptf  6971  fvmptnf  6972  eqfnfv2f  6989  ralrnmptw  7048  ralrnmpt  7050  dffo3f  7060  ffnfvf  7074  funiunfvf  7205  dff13f  7212  nfiso  7279  nfrdg  8359  rdgsucmptf  8373  rdgsucmptnf  8374  frsucmpt  8383  frsucmptn  8384  ttrclselem1  9654  ttrclselem2  9655  rankidb  9729  rankval4  9796  dfac8clem  9961  cardaleph  10018  hsmexlem2  10356  axcc2  10366  uniimadomf  10474  nfseq  13952  seqof2  14001  rlim2  15438  nfsum1  15632  nfsum  15633  sumeq2ii  15635  fsumrelem  15749  o1fsum  15755  nfcprod1  15850  nfcprod  15851  fprodefsum  16037  prdsbas3  17420  prdsdsval2  17423  yonedalem4b  18213  gsum2d2lem  19879  coe1fzgsumdlem  22166  evl1gsumdlem  22219  ptcldmpt  23477  ptcnp  23485  cnmpt11  23526  cnmpt21  23534  cnmptk2  23549  prdsdsf  24231  prdsxmet  24233  ovolfiniun  25378  ovoliunlem3  25381  ovoliun  25382  ovoliun2  25383  ovoliunnul  25384  volfiniun  25424  voliun  25431  mbfsup  25541  mbflim  25545  itg2splitlem  25625  itg2split  25626  itg2cnlem1  25638  isibl2  25643  nfitg1  25651  nfitg  25652  cbvitg  25653  itgabs  25712  dvlipcn  25875  lhop2  25896  dvfsumabs  25905  dvfsumrlim  25914  itgparts  25930  itgsubstlem  25931  ulmss  26282  itgulm2  26294  lgamgulmlem2  26916  lgamgulmlem6  26920  lgamgulm2  26922  lgseisenlem2  27263  dchrisumlem3  27378  sltval2  27544  nfseqs  28157  cnlnadjlem5  31973  dfimafnf  32533  2ndresdju  32546  esumfzf  34032  voliune  34192  volfiniune  34193  bnj1534  34816  bnj1542  34820  bnj958  34903  bnj1000  34904  bnj1446  35008  bnj1447  35009  bnj1448  35010  bnj1466  35016  bnj1467  35017  bnj1519  35028  bnj1520  35029  bnj1529  35033  onvf1odlem2  35064  cvmcov  35223  rdgssun  37339  exrecfnlem  37340  finxpreclem2  37351  finxpreclem6  37357  poimirlem23  37610  poimirlem27  37614  itgabsnc  37656  riotaocN  39175  cdleme32d  40411  cdleme32f  40413  ltrniotaval  40548  cdlemksv2  40814  cdlemkuv2  40834  cdlemk36  40880  cdlemk38  40882  cdlemk19x  40910  cdlemk11t  40913  evl1gprodd  42078  mzpsubst  42709  aomclem8  43023  mnringmulrcld  44190  binomcxplemdvbinom  44315  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  nfrelp  44912  permaxrep  44969  permaxsep  44970  evth2f  44982  fvelrnbf  44985  evthf  44994  rfcnpre3  45000  rfcnpre4  45001  rfcnnnub  45003  refsum2cnlem1  45004  allbutfiinf  45389  monoordxr  45451  monoord2xr  45453  caucvgbf  45458  cvgcaule  45460  fmul01  45551  fmuldfeqlem1  45553  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  fmul01lt1  45557  cncfmptss  45558  mulc1cncfg  45560  expcnfg  45562  fprodabs2  45566  climmulf  45575  climexp  45576  climsuse  45579  climrecf  45580  climinff  45582  climaddf  45586  mullimc  45587  idlimc  45597  limcperiod  45599  neglimc  45618  addlimc  45619  0ellimcdiv  45620  fnlimfv  45634  climreclf  45635  fnlimcnv  45638  fnlimfvre  45645  fnlimfvre2  45648  fnlimf  45649  fnlimabslt  45650  climfveqf  45651  climmptf  45652  climeldmeqf  45654  limsupref  45656  limsupbnd1f  45657  climbddf  45658  climeqf  45659  limsuppnfd  45673  climinf2  45678  limsuppnf  45682  limsupubuz  45684  climinfmpt  45686  limsupmnf  45692  limsupequz  45694  limsupre2  45696  limsupmnfuz  45698  limsupre3  45704  limsupre3uz  45707  limsupreuz  45708  climuz  45715  lmbr3  45718  limsupgt  45749  liminfvalxr  45754  liminfreuz  45774  liminflt  45776  xlimpnfxnegmnf  45785  liminfpnfuz  45787  xlimmnf  45812  xlimpnf  45813  dfxlim2  45819  xlimpnfxnegmnf2  45829  cncfshift  45845  icccncfext  45858  cncficcgt0  45859  cncfiooicclem1  45864  dvnmul  45914  dvnprodlem1  45917  itgsubsticclem  45946  stoweidlem3  45974  stoweidlem23  45994  stoweidlem26  45997  stoweidlem28  45999  stoweidlem29  46000  stoweidlem31  46002  stoweidlem34  46005  stoweidlem36  46007  stoweidlem42  46013  stoweidlem48  46019  stoweidlem51  46022  stoweidlem52  46023  stoweidlem59  46030  wallispilem5  46040  stirlinglem4  46048  stirlinglem11  46055  stirlinglem12  46056  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  fourierdlem20  46098  fourierdlem31  46109  fourierdlem79  46156  fourierdlem89  46166  fourierdlem91  46168  fourierdlem112  46189  fourierdlem115  46192  fourierd  46193  fourierclimd  46194  etransclem2  46207  etransclem48  46253  sge0revalmpt  46349  sge0fsummpt  46361  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0iunmpt  46389  sge0xadd  46406  sge0fsummptf  46407  sge0gtfsumgt  46414  iundjiun  46431  meadjiun  46437  voliunsge0lem  46443  meaiunincf  46454  meaiuninc3  46456  omeiunle  46488  omeiunltfirp  46490  ovncvrrp  46535  vonioo  46653  vonicc  46656  vonn0ioo2  46661  vonn0icc2  46663  pimltmnf2f  46668  pimgtpnf2f  46676  pimltpnf2f  46683  pimgtmnf2  46685  pimdecfgtioc  46686  issmff  46705  smfpimltxrmptf  46729  smfpreimagtf  46739  smflim  46748  smfpimgtxr  46751  smfpimgtxrmptf  46755  smfmullem4  46765  smflim2  46777  smfpimcclem  46778  smfpimcc  46779  smfsup  46785  smfsupmpt  46786  smfsupxr  46787  smfinflem  46788  smfinf  46789  smflimsuplem2  46792  smflimsuplem5  46795  smflimsuplem7  46797  smflimsup  46799  smfliminf  46802  fsupdm  46813  smfsupdmmbllem  46815  finfdm  46817  smfinfdmmbllem  46819  nfafv  47110  nfsetrecs  49648  setrec2fun  49654