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  18217  gsum2d2lem  19887  coe1fzgsumdlem  22223  evl1gsumdlem  22276  ptcldmpt  23534  ptcnp  23542  cnmpt11  23583  cnmpt21  23591  cnmptk2  23606  prdsdsf  24288  prdsxmet  24290  ovolfiniun  25435  ovoliunlem3  25438  ovoliun  25439  ovoliun2  25440  ovoliunnul  25441  volfiniun  25481  voliun  25488  mbfsup  25598  mbflim  25602  itg2splitlem  25682  itg2split  25683  itg2cnlem1  25695  isibl2  25700  nfitg1  25708  nfitg  25709  cbvitg  25710  itgabs  25769  dvlipcn  25932  lhop2  25953  dvfsumabs  25962  dvfsumrlim  25971  itgparts  25987  itgsubstlem  25988  ulmss  26339  itgulm2  26351  lgamgulmlem2  26973  lgamgulmlem6  26977  lgamgulm2  26979  lgseisenlem2  27320  dchrisumlem3  27435  sltval2  27601  nfseqs  28221  cnlnadjlem5  32050  dfimafnf  32610  2ndresdju  32623  esumfzf  34052  voliune  34212  volfiniune  34213  bnj1534  34836  bnj1542  34840  bnj958  34923  bnj1000  34924  bnj1446  35028  bnj1447  35029  bnj1448  35030  bnj1466  35036  bnj1467  35037  bnj1519  35048  bnj1520  35049  bnj1529  35053  onvf1odlem2  35084  cvmcov  35243  rdgssun  37359  exrecfnlem  37360  finxpreclem2  37371  finxpreclem6  37377  poimirlem23  37630  poimirlem27  37634  itgabsnc  37676  riotaocN  39195  cdleme32d  40431  cdleme32f  40433  ltrniotaval  40568  cdlemksv2  40834  cdlemkuv2  40854  cdlemk36  40900  cdlemk38  40902  cdlemk19x  40930  cdlemk11t  40933  evl1gprodd  42098  mzpsubst  42729  aomclem8  43043  mnringmulrcld  44210  binomcxplemdvbinom  44335  binomcxplemdvsum  44337  binomcxplemnotnn0  44338  nfrelp  44932  permaxrep  44989  permaxsep  44990  evth2f  45002  fvelrnbf  45005  evthf  45014  rfcnpre3  45020  rfcnpre4  45021  rfcnnnub  45023  refsum2cnlem1  45024  allbutfiinf  45409  monoordxr  45471  monoord2xr  45473  caucvgbf  45478  cvgcaule  45480  fmul01  45571  fmuldfeqlem1  45573  fmuldfeq  45574  fmul01lt1lem1  45575  fmul01lt1lem2  45576  fmul01lt1  45577  cncfmptss  45578  mulc1cncfg  45580  expcnfg  45582  fprodabs2  45586  climmulf  45595  climexp  45596  climsuse  45599  climrecf  45600  climinff  45602  climaddf  45606  mullimc  45607  idlimc  45617  limcperiod  45619  neglimc  45638  addlimc  45639  0ellimcdiv  45640  fnlimfv  45654  climreclf  45655  fnlimcnv  45658  fnlimfvre  45665  fnlimfvre2  45668  fnlimf  45669  fnlimabslt  45670  climfveqf  45671  climmptf  45672  climeldmeqf  45674  limsupref  45676  limsupbnd1f  45677  climbddf  45678  climeqf  45679  limsuppnfd  45693  climinf2  45698  limsuppnf  45702  limsupubuz  45704  climinfmpt  45706  limsupmnf  45712  limsupequz  45714  limsupre2  45716  limsupmnfuz  45718  limsupre3  45724  limsupre3uz  45727  limsupreuz  45728  climuz  45735  lmbr3  45738  limsupgt  45769  liminfvalxr  45774  liminfreuz  45794  liminflt  45796  xlimpnfxnegmnf  45805  liminfpnfuz  45807  xlimmnf  45832  xlimpnf  45833  dfxlim2  45839  xlimpnfxnegmnf2  45849  cncfshift  45865  icccncfext  45878  cncficcgt0  45879  cncfiooicclem1  45884  dvnmul  45934  dvnprodlem1  45937  itgsubsticclem  45966  stoweidlem3  45994  stoweidlem23  46014  stoweidlem26  46017  stoweidlem28  46019  stoweidlem29  46020  stoweidlem31  46022  stoweidlem34  46025  stoweidlem36  46027  stoweidlem42  46033  stoweidlem48  46039  stoweidlem51  46042  stoweidlem52  46043  stoweidlem59  46050  wallispilem5  46060  stirlinglem4  46068  stirlinglem11  46075  stirlinglem12  46076  stirlinglem13  46077  stirlinglem14  46078  stirlinglem15  46079  fourierdlem20  46118  fourierdlem31  46129  fourierdlem79  46176  fourierdlem89  46186  fourierdlem91  46188  fourierdlem112  46209  fourierdlem115  46212  fourierd  46213  fourierclimd  46214  etransclem2  46227  etransclem48  46273  sge0revalmpt  46369  sge0fsummpt  46381  sge0iunmptlemfi  46404  sge0iunmptlemre  46406  sge0iunmpt  46409  sge0xadd  46426  sge0fsummptf  46427  sge0gtfsumgt  46434  iundjiun  46451  meadjiun  46457  voliunsge0lem  46463  meaiunincf  46474  meaiuninc3  46476  omeiunle  46508  omeiunltfirp  46510  ovncvrrp  46555  vonioo  46673  vonicc  46676  vonn0ioo2  46681  vonn0icc2  46683  pimltmnf2f  46688  pimgtpnf2f  46696  pimltpnf2f  46703  pimgtmnf2  46705  pimdecfgtioc  46706  issmff  46725  smfpimltxrmptf  46749  smfpreimagtf  46759  smflim  46768  smfpimgtxr  46771  smfpimgtxrmptf  46775  smfmullem4  46785  smflim2  46797  smfpimcclem  46798  smfpimcc  46799  smfsup  46805  smfsupmpt  46806  smfsupxr  46807  smfinflem  46808  smfinf  46809  smflimsuplem2  46812  smflimsuplem5  46815  smflimsuplem7  46817  smflimsup  46819  smfliminf  46822  fsupdm  46833  smfsupdmmbllem  46835  finfdm  46837  smfinfdmmbllem  46839  nfafv  47130  nfsetrecs  49668  setrec2fun  49674