Theorem nffv 6682

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 6365	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2979	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5115	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6320	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2977	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2963   class class class wbr 5068  ℩cio 6314  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365

This theorem is referenced by:  nffvmpt1  6683  nffvd  6684  fvelimad  6734  dffn5f  6738  fvmptss  6782  fvmptex  6784  fvmptf  6791  fvmptnf  6792  eqfnfv2f  6808  ralrnmptw  6862  ralrnmpt  6864  ffnfvf  6885  funiunfvf  7010  dff13f  7016  nfiso  7077  nfwrecs  7951  nfrdg  8052  rdgsucmptf  8066  rdgsucmptnf  8067  frsucmpt  8075  frsucmptn  8076  rankidb  9231  rankval4  9298  dfac8clem  9460  cardaleph  9517  hsmexlem2  9851  axcc2  9861  uniimadomf  9969  nfseq  13382  seqof2  13431  rlim2  14855  nfsum1  15048  nfsumw  15049  nfsum  15050  sumeq2ii  15052  fsumrelem  15164  o1fsum  15170  nfcprod1  15266  nfcprod  15267  fprodefsum  15450  prdsbas3  16756  prdsdsval2  16759  yonedalem4b  17528  gsum2d2lem  19095  coe1fzgsumdlem  20471  evl1gsumdlem  20521  ptcldmpt  22224  ptcnp  22232  cnmpt11  22273  cnmpt21  22281  cnmptk2  22296  prdsdsf  22979  prdsxmet  22981  ovolfiniun  24104  ovoliunlem3  24107  ovoliun  24108  ovoliun2  24109  ovoliunnul  24110  volfiniun  24150  voliun  24157  mbfsup  24267  mbflim  24271  itg2splitlem  24351  itg2split  24352  itg2cnlem1  24364  isibl2  24369  nfitg1  24376  nfitg  24377  cbvitg  24378  itgabs  24437  dvlipcn  24593  lhop2  24614  dvfsumabs  24622  dvfsumrlim  24630  itgparts  24646  itgsubstlem  24647  ulmss  24987  itgulm2  24999  lgamgulmlem2  25609  lgamgulmlem6  25613  lgamgulm2  25615  lgseisenlem2  25954  dchrisumlem3  26069  cnlnadjlem5  29850  dfimafnf  30383  esumfzf  31330  voliune  31490  volfiniune  31491  bnj1534  32127  bnj1542  32131  bnj958  32214  bnj1000  32215  bnj1446  32319  bnj1447  32320  bnj1448  32321  bnj1466  32327  bnj1467  32328  bnj1519  32339  bnj1520  32340  bnj1529  32344  cvmcov  32512  trpredlem1  33068  trpredrec  33079  sltval2  33165  rdgssun  34661  exrecfnlem  34662  finxpreclem2  34673  finxpreclem6  34679  poimirlem23  34917  poimirlem27  34921  itgabsnc  34963  riotaocN  36347  cdleme32d  37582  cdleme32f  37584  ltrniotaval  37719  cdlemksv2  37985  cdlemkuv2  38005  cdlemk36  38051  cdlemk38  38053  cdlemk19x  38081  cdlemk11t  38084  mzpsubst  39352  aomclem8  39668  binomcxplemdvbinom  40692  binomcxplemdvsum  40694  binomcxplemnotnn0  40695  evth2f  41279  fvelrnbf  41282  evthf  41291  rfcnpre3  41297  rfcnpre4  41298  rfcnnnub  41300  refsum2cnlem1  41301  dffo3f  41445  allbutfiinf  41701  monoordxr  41766  monoord2xr  41768  fmul01  41868  fmuldfeqlem1  41870  fmuldfeq  41871  fmul01lt1lem1  41872  fmul01lt1lem2  41873  fmul01lt1  41874  cncfmptss  41875  mulc1cncfg  41877  expcnfg  41879  fprodabs2  41883  climmulf  41892  climexp  41893  climsuse  41896  climrecf  41897  climinff  41899  climaddf  41903  mullimc  41904  idlimc  41914  limcperiod  41916  neglimc  41935  addlimc  41936  0ellimcdiv  41937  fnlimfv  41951  climreclf  41952  fnlimcnv  41955  fnlimfvre  41962  fnlimfvre2  41965  fnlimf  41966  fnlimabslt  41967  climfveqf  41968  climmptf  41969  climeldmeqf  41971  limsupref  41973  limsupbnd1f  41974  climbddf  41975  climeqf  41976  limsuppnfd  41990  climinf2  41995  limsuppnf  41999  limsupubuz  42001  climinfmpt  42003  limsupmnf  42009  limsupequz  42011  limsupre2  42013  limsupmnfuz  42015  limsupre3  42021  limsupre3uz  42024  limsupreuz  42025  climuz  42032  lmbr3  42035  limsupgt  42066  liminfvalxr  42071  liminfreuz  42091  liminflt  42093  xlimpnfxnegmnf  42102  liminfpnfuz  42104  xlimmnf  42129  xlimpnf  42130  dfxlim2  42136  xlimpnfxnegmnf2  42146  cncfshift  42164  icccncfext  42177  cncficcgt0  42178  cncfiooicclem1  42183  dvnmul  42235  dvnprodlem1  42238  itgsubsticclem  42267  stoweidlem3  42295  stoweidlem23  42315  stoweidlem26  42318  stoweidlem28  42320  stoweidlem29  42321  stoweidlem31  42323  stoweidlem34  42326  stoweidlem36  42328  stoweidlem42  42334  stoweidlem48  42340  stoweidlem51  42343  stoweidlem52  42344  stoweidlem59  42351  wallispilem5  42361  stirlinglem4  42369  stirlinglem11  42376  stirlinglem12  42377  stirlinglem13  42378  stirlinglem14  42379  stirlinglem15  42380  fourierdlem20  42419  fourierdlem31  42430  fourierdlem79  42477  fourierdlem89  42487  fourierdlem91  42489  fourierdlem112  42510  fourierdlem115  42513  fourierd  42514  fourierclimd  42515  etransclem2  42528  etransclem48  42574  sge0revalmpt  42667  sge0fsummpt  42679  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  sge0iunmpt  42707  sge0xadd  42724  sge0fsummptf  42725  sge0gtfsumgt  42732  iundjiun  42749  meadjiun  42755  voliunsge0lem  42761  meaiunincf  42772  meaiuninc3  42774  omeiunle  42806  omeiunltfirp  42808  ovncvrrp  42853  vonioo  42971  vonicc  42974  vonn0ioo2  42979  vonn0icc2  42981  pimltmnf2  42986  pimgtpnf2  42992  pimltpnf2  42998  pimgtmnf2  42999  pimdecfgtioc  43000  issmff  43018  smfpimltxrmpt  43042  smfpreimagtf  43051  smflim  43060  smfpimgtxr  43063  smfpimgtxrmpt  43067  smfmullem4  43076  smflim2  43087  smfpimcclem  43088  smfpimcc  43089  smfsup  43095  smfsupmpt  43096  smfsupxr  43097  smfinflem  43098  smfinf  43099  smfinfmpt  43100  smflimsuplem2  43102  smflimsuplem5  43105  smflimsuplem7  43107  smflimsup  43109  smfliminf  43112  nfafv  43342  nfsetrecs  44796  setrec2fun  44802