Theorem nffv 6888

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 6541	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2922	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5152	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6493	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2920	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

This proof depends on syntax axioms:  Ⅎwnfc 2907   class class class wbr 5103  ℩cio 6487  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541

This theorem is used by:  nffvmpt1  6889  nffvd  6890  fvelimad  6945  dffn5f  6949  fvmptss  6999  fvmptex  7001  fvmptf  7008  fvmptnf  7009  eqfnfv2f  7026  ralrnmptw  7087  ralrnmpt  7089  dffo3f  7099  ffnfvf  7113  funiunfvf  7246  dff13f  7252  nfiso  7323  nfrdg  8403  rdgsucmptf  8417  rdgsucmptnf  8418  frsucmpt  8427  frsucmptn  8428  ttrclselem1  9704  ttrclselem2  9705  rankidb  9782  rankval4  9849  dfac8clem  10035  cardaleph  10092  hsmexlem2  10429  axcc2  10439  uniimadomf  10553  nfseq  14075  seqof2  14124  rlim2  15583  nfsum1  15777  nfsum  15778  sumeq2ii  15780  fsumrelem  15894  o1fsum  15900  nfcprod1  15997  nfcprod  15998  fprodefsum  16181  prdsbas3  17566  prdsdsval2  17569  yonedalem4b  18364  gsum2d2lem  20100  coe1fzgsumdlem  22528  evl1gsumdlem  22581  ptcldmpt  23840  ptcnp  23848  cnmpt11  23889  cnmpt21  23897  cnmptk2  23912  prdsdsf  24593  prdsxmet  24595  ovolfiniun  25729  ovoliunlem3  25732  ovoliun  25733  ovoliun2  25734  ovoliunnul  25735  volfiniun  25775  voliun  25782  mbfsup  25892  mbflim  25896  itg2splitlem  25976  itg2split  25977  itg2cnlem1  25989  isibl2  25994  nfitg1  26001  nfitg  26002  cbvitg  26003  itgabs  26062  dvlipcn  26221  lhop2  26242  dvfsumabs  26250  dvfsumrlim  26258  itgparts  26274  itgsubstlem  26275  ulmss  26633  itgulm2  26645  lgamgulmlem2  27266  lgamgulmlem6  27270  lgamgulm2  27272  lgseisenlem2  27612  dchrisumlem3  27727  ltsval2  27892  nfseqs  28552  cnlnadjlem5  32552  dfimafnf  33109  2ndresdju  33122  deg1prod  33993  esumfzf  34579  voliune  34740  volfiniune  34741  bnj1534  35362  bnj1542  35366  bnj958  35449  bnj1000  35450  bnj1446  35554  bnj1447  35555  bnj1448  35556  bnj1466  35562  bnj1467  35563  bnj1519  35574  bnj1520  35575  bnj1529  35579  rankval4b  35607  onvf1odlem2  35701  vonf1oonfo  35712  cvmcov  35842  rdgssun  38132  exrecfnlem  38133  finxpreclem2  38144  finxpreclem6  38150  poimirlem23  38392  poimirlem27  38396  itgabsnc  38438  riotaocN  40082  cdleme32d  41317  cdleme32f  41319  ltrniotaval  41454  cdlemksv2  41720  cdlemkuv2  41740  cdlemk36  41786  cdlemk38  41788  cdlemk19x  41816  cdlemk11t  41819  evl1gprodd  42983  mzpsubst  43593  aomclem8  43902  mnringmulrcld  45066  binomcxplemdvbinom  45177  binomcxplemdvsum  45179  binomcxplemnotnn0  45180  nfrelp  45772  permaxrep  45829  permaxsep  45830  evth2f  45849  fvelrnbf  45852  evthf  45861  rfcnpre3  45867  rfcnpre4  45868  rfcnnnub  45870  refsum2cnlem1  45871  allbutfiinf  46248  monoordxr  46310  monoord2xr  46312  caucvgbf  46317  cvgcaule  46319  fmul01  46410  fmuldfeqlem1  46412  fmuldfeq  46413  fmul01lt1lem1  46414  fmul01lt1lem2  46415  fmul01lt1  46416  cncfmptss  46417  mulc1cncfg  46419  expcnfg  46421  fprodabs2  46425  climmulf  46434  climexp  46435  climsuse  46438  climrecf  46439  climinff  46441  climaddf  46445  mullimc  46446  idlimc  46456  limcperiod  46458  neglimc  46475  addlimc  46476  0ellimcdiv  46477  fnlimfv  46491  climreclf  46492  fnlimcnv  46495  fnlimfvre  46502  fnlimfvre2  46505  fnlimf  46506  fnlimabslt  46507  climfveqf  46508  climmptf  46509  climeldmeqf  46511  limsupref  46513  limsupbnd1f  46514  climbddf  46515  climeqf  46516  limsuppnfd  46530  climinf2  46535  limsuppnf  46539  limsupubuz  46541  climinfmpt  46543  limsupmnf  46549  limsupequz  46551  limsupre2  46553  limsupmnfuz  46555  limsupre3  46561  limsupre3uz  46564  limsupreuz  46565  climuz  46572  lmbr3  46575  limsupgt  46606  liminfvalxr  46611  liminfreuz  46631  liminflt  46633  xlimpnfxnegmnf  46642  liminfpnfuz  46644  xlimmnf  46669  xlimpnf  46670  dfxlim2  46676  xlimpnfxnegmnf2  46686  cncfshift  46702  icccncfext  46715  cncficcgt0  46716  cncfiooicclem1  46721  dvnmul  46771  dvnprodlem1  46774  itgsubsticclem  46803  stoweidlem3  46831  stoweidlem23  46851  stoweidlem26  46854  stoweidlem28  46856  stoweidlem29  46857  stoweidlem31  46859  stoweidlem34  46862  stoweidlem36  46864  stoweidlem42  46870  stoweidlem48  46876  stoweidlem51  46879  stoweidlem52  46880  stoweidlem59  46887  wallispilem5  46897  stirlinglem4  46905  stirlinglem11  46912  stirlinglem12  46913  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  fourierdlem20  46955  fourierdlem31  46966  fourierdlem79  47013  fourierdlem89  47023  fourierdlem91  47025  fourierdlem112  47046  fourierdlem115  47049  fourierd  47050  fourierclimd  47051  etransclem2  47064  etransclem48  47110  sge0revalmpt  47206  sge0fsummpt  47218  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0iunmpt  47246  sge0xadd  47263  sge0fsummptf  47264  sge0gtfsumgt  47271  iundjiun  47288  meadjiun  47294  voliunsge0lem  47300  meaiunincf  47311  meaiuninc3  47313  omeiunle  47345  omeiunltfirp  47347  ovncvrrp  47392  vonioo  47510  vonicc  47513  vonn0ioo2  47518  vonn0icc2  47520  pimltmnf2f  47525  pimgtpnf2f  47533  pimltpnf2f  47540  pimgtmnf2  47542  pimdecfgtioc  47543  issmff  47562  smfpimltxrmptf  47586  smfpreimagtf  47596  smflim  47605  smfpimgtxr  47608  smfpimgtxrmptf  47612  smfmullem4  47622  smflim2  47634  smfpimcclem  47635  smfpimcc  47636  smfsup  47642  smfsupmpt  47643  smfsupxr  47644  smfinflem  47645  smfinf  47646  smflimsuplem2  47649  smflimsuplem5  47652  smflimsuplem7  47654  smflimsup  47656  smfliminf  47659  fsupdm  47670  smfsupdmmbllem  47672  finfdm  47674  smfinfdmmbllem  47676  nfafv  48024  nfsetrecs  50612  setrec2fun  50618