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 6506	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2898	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5132	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6458	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2896	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2883   class class class wbr 5085  ℩cio 6452  ‘cfv 6498

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506

This theorem is referenced by:  nffvmpt1  6851  nffvd  6852  fvelimad  6907  dffn5f  6911  fvmptss  6960  fvmptex  6962  fvmptf  6969  fvmptnf  6970  eqfnfv2f  6987  ralrnmptw  7046  ralrnmpt  7048  dffo3f  7058  ffnfvf  7072  funiunfvf  7204  dff13f  7210  nfiso  7277  nfrdg  8353  rdgsucmptf  8367  rdgsucmptnf  8368  frsucmpt  8377  frsucmptn  8378  ttrclselem1  9646  ttrclselem2  9647  rankidb  9724  rankval4  9791  dfac8clem  9954  cardaleph  10011  hsmexlem2  10349  axcc2  10359  uniimadomf  10467  nfseq  13973  seqof2  14022  rlim2  15458  nfsum1  15652  nfsum  15653  sumeq2ii  15655  fsumrelem  15770  o1fsum  15776  nfcprod1  15873  nfcprod  15874  fprodefsum  16060  prdsbas3  17444  prdsdsval2  17447  yonedalem4b  18242  gsum2d2lem  19948  coe1fzgsumdlem  22268  evl1gsumdlem  22321  ptcldmpt  23579  ptcnp  23587  cnmpt11  23628  cnmpt21  23636  cnmptk2  23651  prdsdsf  24332  prdsxmet  24334  ovolfiniun  25468  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  ovoliunnul  25474  volfiniun  25514  voliun  25521  mbfsup  25631  mbflim  25635  itg2splitlem  25715  itg2split  25716  itg2cnlem1  25728  isibl2  25733  nfitg1  25741  nfitg  25742  cbvitg  25743  itgabs  25802  dvlipcn  25961  lhop2  25982  dvfsumabs  25990  dvfsumrlim  25998  itgparts  26014  itgsubstlem  26015  ulmss  26362  itgulm2  26374  lgamgulmlem2  26993  lgamgulmlem6  26997  lgamgulm2  26999  lgseisenlem2  27339  dchrisumlem3  27454  ltsval2  27620  nfseqs  28279  cnlnadjlem5  32142  dfimafnf  32709  2ndresdju  32722  deg1prod  33643  esumfzf  34213  voliune  34373  volfiniune  34374  bnj1534  34995  bnj1542  34999  bnj958  35082  bnj1000  35083  bnj1446  35187  bnj1447  35188  bnj1448  35189  bnj1466  35195  bnj1467  35196  bnj1519  35207  bnj1520  35208  bnj1529  35212  rankval4b  35243  onvf1odlem2  35286  cvmcov  35445  rdgssun  37694  exrecfnlem  37695  finxpreclem2  37706  finxpreclem6  37712  poimirlem23  37964  poimirlem27  37968  itgabsnc  38010  riotaocN  39655  cdleme32d  40890  cdleme32f  40892  ltrniotaval  41027  cdlemksv2  41293  cdlemkuv2  41313  cdlemk36  41359  cdlemk38  41361  cdlemk19x  41389  cdlemk11t  41392  evl1gprodd  42556  mzpsubst  43180  aomclem8  43489  mnringmulrcld  44655  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  nfrelp  45376  permaxrep  45433  permaxsep  45434  evth2f  45446  fvelrnbf  45449  evthf  45458  rfcnpre3  45464  rfcnpre4  45465  rfcnnnub  45467  refsum2cnlem1  45468  allbutfiinf  45848  monoordxr  45910  monoord2xr  45912  caucvgbf  45917  cvgcaule  45919  fmul01  46010  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  fmul01lt1  46016  cncfmptss  46017  mulc1cncfg  46019  expcnfg  46021  fprodabs2  46025  climmulf  46034  climexp  46035  climsuse  46038  climrecf  46039  climinff  46041  climaddf  46045  mullimc  46046  idlimc  46056  limcperiod  46058  neglimc  46075  addlimc  46076  0ellimcdiv  46077  fnlimfv  46091  climreclf  46092  fnlimcnv  46095  fnlimfvre  46102  fnlimfvre2  46105  fnlimf  46106  fnlimabslt  46107  climfveqf  46108  climmptf  46109  climeldmeqf  46111  limsupref  46113  limsupbnd1f  46114  climbddf  46115  climeqf  46116  limsuppnfd  46130  climinf2  46135  limsuppnf  46139  limsupubuz  46141  climinfmpt  46143  limsupmnf  46149  limsupequz  46151  limsupre2  46153  limsupmnfuz  46155  limsupre3  46161  limsupre3uz  46164  limsupreuz  46165  climuz  46172  lmbr3  46175  limsupgt  46206  liminfvalxr  46211  liminfreuz  46231  liminflt  46233  xlimpnfxnegmnf  46242  liminfpnfuz  46244  xlimmnf  46269  xlimpnf  46270  dfxlim2  46276  xlimpnfxnegmnf2  46286  cncfshift  46302  icccncfext  46315  cncficcgt0  46316  cncfiooicclem1  46321  dvnmul  46371  dvnprodlem1  46374  itgsubsticclem  46403  stoweidlem3  46431  stoweidlem23  46451  stoweidlem26  46454  stoweidlem28  46456  stoweidlem29  46457  stoweidlem31  46459  stoweidlem34  46462  stoweidlem36  46464  stoweidlem42  46470  stoweidlem48  46476  stoweidlem51  46479  stoweidlem52  46480  stoweidlem59  46487  wallispilem5  46497  stirlinglem4  46505  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  fourierdlem20  46555  fourierdlem31  46566  fourierdlem79  46613  fourierdlem89  46623  fourierdlem91  46625  fourierdlem112  46646  fourierdlem115  46649  fourierd  46650  fourierclimd  46651  etransclem2  46664  etransclem48  46710  sge0revalmpt  46806  sge0fsummpt  46818  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0xadd  46863  sge0fsummptf  46864  sge0gtfsumgt  46871  iundjiun  46888  meadjiun  46894  voliunsge0lem  46900  meaiunincf  46911  meaiuninc3  46913  omeiunle  46945  omeiunltfirp  46947  ovncvrrp  46992  vonioo  47110  vonicc  47113  vonn0ioo2  47118  vonn0icc2  47120  pimltmnf2f  47125  pimgtpnf2f  47133  pimltpnf2f  47140  pimgtmnf2  47142  pimdecfgtioc  47143  issmff  47162  smfpimltxrmptf  47186  smfpreimagtf  47196  smflim  47205  smfpimgtxr  47208  smfpimgtxrmptf  47212  smfmullem4  47222  smflim2  47234  smfpimcclem  47235  smfpimcc  47236  smfsup  47242  smfsupmpt  47243  smfsupxr  47244  smfinflem  47245  smfinf  47246  smflimsuplem2  47249  smflimsuplem5  47252  smflimsuplem7  47254  smflimsup  47256  smfliminf  47259  fsupdm  47270  smfsupdmmbllem  47272  finfdm  47274  smfinfdmmbllem  47276  nfafv  47584  nfsetrecs  50161  setrec2fun  50167