Theorem nffv 6926

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 6574	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2926	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5158	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6524	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2924	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

This proof depends on syntax axioms:  Ⅎwnfc 2911   class class class wbr 5108  ℩cio 6518  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574

This theorem is used by:  nffvmpt1  6927  nffvd  6928  fvelimad  6983  dffn5f  6987  fvmptss  7037  fvmptex  7039  fvmptf  7046  fvmptnf  7047  eqfnfv2f  7064  ralrnmptw  7126  ralrnmpt  7128  dffo3f  7138  ffnfvf  7152  funiunfvf  7284  dff13f  7290  nfiso  7361  nfrdg  8460  rdgsucmptf  8474  rdgsucmptnf  8475  frsucmpt  8484  frsucmptn  8485  ttrclselem1  9763  ttrclselem2  9764  rankidb  9845  rankval4b  9917  rankval4  9921  setrec2fun  10010  dfac8clem  10150  cardaleph  10207  hsmexlem2  10544  axcc2  10554  uniimadomf  10668  nfseq  14194  seqof2  14243  rlim2  15707  nfsum1  15901  nfsum  15902  sumeq2ii  15904  fsumrelem  16018  o1fsum  16024  nfcprod1  16121  nfcprod  16122  fprodefsum  16305  prdsbas3  17702  prdsdsval2  17705  yonedalem4b  18500  gsum2d2lem  20238  coe1fzgsumdlem  22676  evl1gsumdlem  22729  ptcldmpt  23988  ptcnp  23996  cnmpt11  24037  cnmpt21  24045  cnmptk2  24060  prdsdsf  24741  prdsxmet  24743  ovolfiniun  25877  ovoliunlem3  25880  ovoliun  25881  ovoliun2  25882  ovoliunnul  25883  volfiniun  25923  voliun  25930  mbfsup  26040  mbflim  26044  itg2splitlem  26124  itg2split  26125  itg2cnlem1  26137  isibl2  26142  nfitg1  26149  nfitg  26150  cbvitg  26151  itgabs  26210  dvlipcn  26369  lhop2  26390  dvfsumabs  26398  dvfsumrlim  26406  itgparts  26422  itgsubstlem  26423  ulmss  26781  itgulm2  26793  lgamgulmlem2  27414  lgamgulmlem6  27418  lgamgulm2  27420  lgseisenlem2  27760  dchrisumlem3  27875  ltsval2  28070  nfseqs  28730  cnlnadjlem5  32730  dfimafnf  33328  2ndresdju  33341  deg1prod  34218  esumfzf  34812  voliune  34973  volfiniune  34974  bnj1534  35594  bnj1542  35598  bnj958  35681  bnj1000  35682  bnj1446  35786  bnj1447  35787  bnj1448  35788  bnj1466  35794  bnj1467  35795  bnj1519  35806  bnj1520  35807  bnj1529  35811  onvf1odlem2  36073  onprcf1acwevdlem2  36087  vonf1oonfo  36090  onprcf1of1ord  36096  srepdflem1  36126  cvmcov  36236  rdgssun  38569  exrecfnlem  38570  finxpreclem2  38581  finxpreclem6  38587  poimirlem23  38829  poimirlem27  38833  itgabsnc  38875  riotaocN  40532  cdleme32d  41767  cdleme32f  41769  ltrniotaval  41904  cdlemksv2  42170  cdlemkuv2  42190  cdlemk36  42236  cdlemk38  42238  cdlemk19x  42266  cdlemk11t  42269  evl1gprodd  43433  mzpsubst  44025  aomclem8  44329  mnringmulrcld  45487  binomcxplemdvbinom  45598  binomcxplemdvsum  45600  binomcxplemnotnn0  45601  nfrelp  46203  permaxrep  46260  permaxsep  46261  evth2f  46306  fvelrnbf  46309  evthf  46318  rfcnpre3  46324  rfcnpre4  46325  rfcnnnub  46327  refsum2cnlem1  46328  allbutfiinf  46703  monoordxr  46765  monoord2xr  46767  caucvgbf  46772  cvgcaule  46774  fmul01  46865  fmuldfeqlem1  46867  fmuldfeq  46868  fmul01lt1lem1  46869  fmul01lt1lem2  46870  fmul01lt1  46871  cncfmptss  46872  mulc1cncfg  46874  expcnfg  46876  fprodabs2  46880  climmulf  46889  climexp  46890  climsuse  46893  climrecf  46894  climinff  46896  climaddf  46900  mullimc  46901  idlimc  46911  limcperiod  46913  neglimc  46930  addlimc  46931  0ellimcdiv  46932  fnlimfv  46946  climreclf  46947  fnlimcnv  46950  fnlimfvre  46957  fnlimfvre2  46960  fnlimf  46961  fnlimabslt  46962  climfveqf  46963  climmptf  46964  climeldmeqf  46966  limsupref  46968  limsupbnd1f  46969  climbddf  46970  climeqf  46971  limsuppnfd  46985  climinf2  46990  limsuppnf  46994  limsupubuz  46996  climinfmpt  46998  limsupmnf  47004  limsupequz  47006  limsupre2  47008  limsupmnfuz  47010  limsupre3  47016  limsupre3uz  47019  limsupreuz  47020  climuz  47027  lmbr3  47030  limsupgt  47061  liminfvalxr  47066  liminfreuz  47086  liminflt  47088  xlimpnfxnegmnf  47097  liminfpnfuz  47099  xlimmnf  47124  xlimpnf  47125  dfxlim2  47131  xlimpnfxnegmnf2  47141  cncfshift  47157  icccncfext  47170  cncficcgt0  47171  cncfiooicclem1  47176  dvnmul  47226  dvnprodlem1  47229  itgsubsticclem  47258  stoweidlem3  47286  stoweidlem23  47306  stoweidlem26  47309  stoweidlem28  47311  stoweidlem29  47312  stoweidlem31  47314  stoweidlem34  47317  stoweidlem36  47319  stoweidlem42  47325  stoweidlem48  47331  stoweidlem51  47334  stoweidlem52  47335  stoweidlem59  47342  wallispilem5  47352  stirlinglem4  47360  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  fourierdlem20  47410  fourierdlem31  47421  fourierdlem79  47468  fourierdlem89  47478  fourierdlem91  47480  fourierdlem112  47501  fourierdlem115  47504  fourierd  47505  fourierclimd  47506  etransclem2  47519  etransclem48  47565  sge0revalmpt  47661  sge0fsummpt  47673  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0iunmpt  47701  sge0xadd  47718  sge0fsummptf  47719  sge0gtfsumgt  47726  iundjiun  47743  meadjiun  47749  voliunsge0lem  47755  meaiunincf  47766  meaiuninc3  47768  omeiunle  47800  omeiunltfirp  47802  ovncvrrp  47847  vonioo  47965  vonicc  47968  vonn0ioo2  47973  vonn0icc2  47975  pimltmnf2f  47980  pimgtpnf2f  47988  pimltpnf2f  47995  pimgtmnf2  47997  pimdecfgtioc  47998  issmff  48017  smfpimltxrmptf  48041  smfpreimagtf  48051  smflim  48060  smfpimgtxr  48063  smfpimgtxrmptf  48067  smfmullem4  48077  smflim2  48089  smfpimcclem  48090  smfpimcc  48091  smfsup  48097  smfsupmpt  48098  smfsupxr  48099  smfinflem  48100  smfinf  48101  smflimsuplem2  48104  smflimsuplem5  48107  smflimsuplem7  48109  smflimsup  48111  smfliminf  48114  fsupdm  48125  smfsupdmmbllem  48127  finfdm  48129  smfinfdmmbllem  48131  nfafv  48479  nfsetrecs  51195