Theorem nffv 6832

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 6489	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2894	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5136	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6441	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2892	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2879   class class class wbr 5089  ℩cio 6435  ‘cfv 6481

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489

This theorem is referenced by:  nffvmpt1  6833  nffvd  6834  fvelimad  6889  dffn5f  6893  fvmptss  6941  fvmptex  6943  fvmptf  6950  fvmptnf  6951  eqfnfv2f  6968  ralrnmptw  7027  ralrnmpt  7029  dffo3f  7039  ffnfvf  7053  funiunfvf  7183  dff13f  7189  nfiso  7256  nfrdg  8333  rdgsucmptf  8347  rdgsucmptnf  8348  frsucmpt  8357  frsucmptn  8358  ttrclselem1  9615  ttrclselem2  9616  rankidb  9693  rankval4  9760  dfac8clem  9923  cardaleph  9980  hsmexlem2  10318  axcc2  10328  uniimadomf  10436  nfseq  13918  seqof2  13967  rlim2  15403  nfsum1  15597  nfsum  15598  sumeq2ii  15600  fsumrelem  15714  o1fsum  15720  nfcprod1  15815  nfcprod  15816  fprodefsum  16002  prdsbas3  17385  prdsdsval2  17388  yonedalem4b  18182  gsum2d2lem  19885  coe1fzgsumdlem  22218  evl1gsumdlem  22271  ptcldmpt  23529  ptcnp  23537  cnmpt11  23578  cnmpt21  23586  cnmptk2  23601  prdsdsf  24282  prdsxmet  24284  ovolfiniun  25429  ovoliunlem3  25432  ovoliun  25433  ovoliun2  25434  ovoliunnul  25435  volfiniun  25475  voliun  25482  mbfsup  25592  mbflim  25596  itg2splitlem  25676  itg2split  25677  itg2cnlem1  25689  isibl2  25694  nfitg1  25702  nfitg  25703  cbvitg  25704  itgabs  25763  dvlipcn  25926  lhop2  25947  dvfsumabs  25956  dvfsumrlim  25965  itgparts  25981  itgsubstlem  25982  ulmss  26333  itgulm2  26345  lgamgulmlem2  26967  lgamgulmlem6  26971  lgamgulm2  26973  lgseisenlem2  27314  dchrisumlem3  27429  sltval2  27595  nfseqs  28217  cnlnadjlem5  32051  dfimafnf  32618  2ndresdju  32631  esumfzf  34082  voliune  34242  volfiniune  34243  bnj1534  34865  bnj1542  34869  bnj958  34952  bnj1000  34953  bnj1446  35057  bnj1447  35058  bnj1448  35059  bnj1466  35065  bnj1467  35066  bnj1519  35077  bnj1520  35078  bnj1529  35082  rankval4b  35111  onvf1odlem2  35148  cvmcov  35307  rdgssun  37420  exrecfnlem  37421  finxpreclem2  37432  finxpreclem6  37438  poimirlem23  37691  poimirlem27  37695  itgabsnc  37737  riotaocN  39256  cdleme32d  40491  cdleme32f  40493  ltrniotaval  40628  cdlemksv2  40894  cdlemkuv2  40914  cdlemk36  40960  cdlemk38  40962  cdlemk19x  40990  cdlemk11t  40993  evl1gprodd  42158  mzpsubst  42789  aomclem8  43102  mnringmulrcld  44269  binomcxplemdvbinom  44394  binomcxplemdvsum  44396  binomcxplemnotnn0  44397  nfrelp  44990  permaxrep  45047  permaxsep  45048  evth2f  45060  fvelrnbf  45063  evthf  45072  rfcnpre3  45078  rfcnpre4  45079  rfcnnnub  45081  refsum2cnlem1  45082  allbutfiinf  45466  monoordxr  45528  monoord2xr  45530  caucvgbf  45535  cvgcaule  45537  fmul01  45628  fmuldfeqlem1  45630  fmuldfeq  45631  fmul01lt1lem1  45632  fmul01lt1lem2  45633  fmul01lt1  45634  cncfmptss  45635  mulc1cncfg  45637  expcnfg  45639  fprodabs2  45643  climmulf  45652  climexp  45653  climsuse  45656  climrecf  45657  climinff  45659  climaddf  45663  mullimc  45664  idlimc  45674  limcperiod  45676  neglimc  45693  addlimc  45694  0ellimcdiv  45695  fnlimfv  45709  climreclf  45710  fnlimcnv  45713  fnlimfvre  45720  fnlimfvre2  45723  fnlimf  45724  fnlimabslt  45725  climfveqf  45726  climmptf  45727  climeldmeqf  45729  limsupref  45731  limsupbnd1f  45732  climbddf  45733  climeqf  45734  limsuppnfd  45748  climinf2  45753  limsuppnf  45757  limsupubuz  45759  climinfmpt  45761  limsupmnf  45767  limsupequz  45769  limsupre2  45771  limsupmnfuz  45773  limsupre3  45779  limsupre3uz  45782  limsupreuz  45783  climuz  45790  lmbr3  45793  limsupgt  45824  liminfvalxr  45829  liminfreuz  45849  liminflt  45851  xlimpnfxnegmnf  45860  liminfpnfuz  45862  xlimmnf  45887  xlimpnf  45888  dfxlim2  45894  xlimpnfxnegmnf2  45904  cncfshift  45920  icccncfext  45933  cncficcgt0  45934  cncfiooicclem1  45939  dvnmul  45989  dvnprodlem1  45992  itgsubsticclem  46021  stoweidlem3  46049  stoweidlem23  46069  stoweidlem26  46072  stoweidlem28  46074  stoweidlem29  46075  stoweidlem31  46077  stoweidlem34  46080  stoweidlem36  46082  stoweidlem42  46088  stoweidlem48  46094  stoweidlem51  46097  stoweidlem52  46098  stoweidlem59  46105  wallispilem5  46115  stirlinglem4  46123  stirlinglem11  46130  stirlinglem12  46131  stirlinglem13  46132  stirlinglem14  46133  stirlinglem15  46134  fourierdlem20  46173  fourierdlem31  46184  fourierdlem79  46231  fourierdlem89  46241  fourierdlem91  46243  fourierdlem112  46264  fourierdlem115  46267  fourierd  46268  fourierclimd  46269  etransclem2  46282  etransclem48  46328  sge0revalmpt  46424  sge0fsummpt  46436  sge0iunmptlemfi  46459  sge0iunmptlemre  46461  sge0iunmpt  46464  sge0xadd  46481  sge0fsummptf  46482  sge0gtfsumgt  46489  iundjiun  46506  meadjiun  46512  voliunsge0lem  46518  meaiunincf  46529  meaiuninc3  46531  omeiunle  46563  omeiunltfirp  46565  ovncvrrp  46610  vonioo  46728  vonicc  46731  vonn0ioo2  46736  vonn0icc2  46738  pimltmnf2f  46743  pimgtpnf2f  46751  pimltpnf2f  46758  pimgtmnf2  46760  pimdecfgtioc  46761  issmff  46780  smfpimltxrmptf  46804  smfpreimagtf  46814  smflim  46823  smfpimgtxr  46826  smfpimgtxrmptf  46830  smfmullem4  46840  smflim2  46852  smfpimcclem  46853  smfpimcc  46854  smfsup  46860  smfsupmpt  46861  smfsupxr  46862  smfinflem  46863  smfinf  46864  smflimsuplem2  46867  smflimsuplem5  46870  smflimsuplem7  46872  smflimsup  46874  smfliminf  46877  fsupdm  46888  smfsupdmmbllem  46890  finfdm  46892  smfinfdmmbllem  46894  nfafv  47175  nfsetrecs  49726  setrec2fun  49732