Theorem nffv 6427

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 6118	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2959	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 4902	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiota 6077	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2957	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2946   class class class wbr 4855  ℩cio 6071  ‘cfv 6110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6073  df-fv 6118

This theorem is referenced by:  nffvmpt1  6428  nffvd  6429  dffn5f  6482  fvmptss  6522  fvmptex  6524  fvmptf  6531  fvmptnf  6532  eqfnfv2f  6546  ralrnmpt  6599  ffnfvf  6620  funiunfvf  6740  dff13f  6746  nfiso  6805  nfwrecs  7653  nfrdg  7755  rdgsucmptf  7769  rdgsucmptnf  7770  frsucmpt  7778  frsucmptn  7779  rankidb  8919  rankval4  8986  dfac8clem  9147  cardaleph  9204  hsmexlem2  9543  axcc2  9553  uniimadomf  9661  nfseq  13053  seqof2  13101  rlim2  14469  nfsum1  14662  nfsum  14663  sumeq2ii  14665  fsumrelem  14780  o1fsum  14786  nfcprod1  14880  nfcprod  14881  fprodefsum  15064  prdsbas3  16365  prdsdsval2  16368  yonedalem4b  17140  gsum2d2lem  18592  coe1fzgsumdlem  19898  evl1gsumdlem  19947  ptcldmpt  21651  ptcnp  21659  cnmpt11  21700  cnmpt21  21708  cnmptk2  21723  prdsdsf  22405  prdsxmet  22407  ovolfiniun  23504  ovoliunlem3  23507  ovoliun  23508  ovoliun2  23509  ovoliunnul  23510  volfiniun  23550  voliun  23557  mbfsup  23667  mbflim  23671  itg2splitlem  23751  itg2split  23752  itg2cnlem1  23764  isibl2  23769  nfitg1  23776  nfitg  23777  cbvitg  23778  itgabs  23837  dvlipcn  23993  lhop2  24014  dvfsumabs  24022  dvfsumrlim  24030  itgparts  24046  itgsubstlem  24047  ulmss  24387  itgulm2  24399  lgamgulmlem2  24992  lgamgulmlem6  24996  lgamgulm2  24998  lgseisenlem2  25337  dchrisumlem3  25416  cnlnadjlem5  29280  dfimafnf  29785  esumfzf  30478  voliune  30639  volfiniune  30640  bnj1534  31267  bnj1542  31271  bnj958  31354  bnj1000  31355  bnj1446  31457  bnj1447  31458  bnj1448  31459  bnj1466  31465  bnj1467  31466  bnj1519  31477  bnj1520  31478  bnj1529  31482  cvmcov  31589  trpredlem1  32068  trpredrec  32079  sltval2  32151  finxpreclem2  33561  finxpreclem6  33567  poimirlem23  33763  poimirlem27  33767  itgabsnc  33809  riotaocN  35007  cdleme32d  36242  cdleme32f  36244  ltrniotaval  36379  cdlemksv2  36645  cdlemkuv2  36665  cdlemk36  36711  cdlemk38  36713  cdlemk19x  36741  cdlemk11t  36744  mzpsubst  37830  aomclem8  38149  binomcxplemdvbinom  39069  binomcxplemdvsum  39071  binomcxplemnotnn0  39072  evth2f  39685  fvelrnbf  39688  evthf  39697  rfcnpre3  39703  rfcnpre4  39704  rfcnnnub  39706  refsum2cnlem1  39707  dffo3f  39870  fvelimad  39959  allbutfiinf  40143  monoordxr  40209  monoord2xr  40211  fmul01  40309  fmuldfeqlem1  40311  fmuldfeq  40312  fmul01lt1lem1  40313  fmul01lt1lem2  40314  fmul01lt1  40315  cncfmptss  40316  mulc1cncfg  40318  expcnfg  40320  fprodabs2  40324  climmulf  40333  climexp  40334  climsuse  40337  climrecf  40338  climinff  40340  climaddf  40344  mullimc  40345  idlimc  40355  limcperiod  40357  neglimc  40376  addlimc  40377  0ellimcdiv  40378  fnlimfv  40392  climreclf  40393  fnlimcnv  40396  fnlimfvre  40403  fnlimfvre2  40406  fnlimf  40407  fnlimabslt  40408  climfveqf  40409  climmptf  40410  climeldmeqf  40412  limsupref  40414  limsupbnd1f  40415  climbddf  40416  climeqf  40417  limsuppnfd  40431  climinf2  40436  limsuppnf  40440  limsupubuz  40442  climinfmpt  40444  limsupmnf  40450  limsupequz  40452  limsupre2  40454  limsupmnfuz  40456  limsupre3  40462  limsupre3uz  40465  limsupreuz  40466  climuz  40473  lmbr3  40476  limsupgt  40507  liminfvalxr  40512  liminfreuz  40532  liminflt  40534  xlimmnf  40564  xlimpnf  40565  dfxlim2  40571  cncfshift  40584  icccncfext  40597  cncficcgt0  40598  cncfiooicclem1  40603  dvnmul  40655  dvnprodlem1  40658  itgsubsticclem  40687  stoweidlem3  40716  stoweidlem23  40736  stoweidlem26  40739  stoweidlem28  40741  stoweidlem29  40742  stoweidlem31  40744  stoweidlem34  40747  stoweidlem36  40749  stoweidlem42  40755  stoweidlem48  40761  stoweidlem51  40764  stoweidlem52  40765  stoweidlem59  40772  wallispilem5  40782  stirlinglem4  40790  stirlinglem11  40797  stirlinglem12  40798  stirlinglem13  40799  stirlinglem14  40800  stirlinglem15  40801  fourierdlem20  40840  fourierdlem31  40851  fourierdlem79  40898  fourierdlem89  40908  fourierdlem91  40910  fourierdlem112  40931  fourierdlem115  40934  fourierd  40935  fourierclimd  40936  etransclem2  40949  etransclem48  40995  sge0revalmpt  41091  sge0fsummpt  41103  sge0iunmptlemfi  41126  sge0iunmptlemre  41128  sge0iunmpt  41131  sge0xadd  41148  sge0fsummptf  41149  sge0gtfsumgt  41156  iundjiun  41173  meadjiun  41179  voliunsge0lem  41185  meaiunincf  41196  meaiuninc3  41198  omeiunle  41230  omeiunltfirp  41232  ovncvrrp  41277  vonioo  41395  vonicc  41398  vonn0ioo2  41403  vonn0icc2  41405  pimltmnf2  41410  pimgtpnf2  41416  pimltpnf2  41422  pimgtmnf2  41423  pimdecfgtioc  41424  issmff  41442  smfpimltxrmpt  41466  smfpreimagtf  41475  smflim  41484  smfpimgtxr  41487  smfpimgtxrmpt  41491  smfmullem4  41500  smflim2  41511  smfpimcclem  41512  smfpimcc  41513  smfsup  41519  smfsupmpt  41520  smfsupxr  41521  smfinflem  41522  smfinf  41523  smfinfmpt  41524  smflimsuplem2  41526  smflimsuplem5  41529  smflimsuplem7  41531  smflimsup  41533  smfliminf  41536  nfafv  41742  nfsetrecs  43018  setrec2fun  43024