Theorem nffv 6893

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

This proof depends on syntax axioms:  Ⅎwnfc 2908   class class class wbr 5103  ℩cio 6491  ‘cfv 6537

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 6493  df-fv 6545

This theorem is used by:  nffvmpt1  6894  nffvd  6895  fvelimad  6950  dffn5f  6954  fvmptss  7004  fvmptex  7006  fvmptf  7013  fvmptnf  7014  eqfnfv2f  7031  ralrnmptw  7092  ralrnmpt  7094  dffo3f  7104  ffnfvf  7118  funiunfvf  7251  dff13f  7257  nfiso  7328  nfrdg  8415  rdgsucmptf  8429  rdgsucmptnf  8430  frsucmpt  8439  frsucmptn  8440  ttrclselem1  9719  ttrclselem2  9720  rankidb  9801  rankval4b  9873  rankval4  9877  setrec2fun  9966  dfac8clem  10104  cardaleph  10161  hsmexlem2  10498  axcc2  10508  uniimadomf  10622  nfseq  14147  seqof2  14196  rlim2  15656  nfsum1  15850  nfsum  15851  sumeq2ii  15853  fsumrelem  15967  o1fsum  15973  nfcprod1  16070  nfcprod  16071  fprodefsum  16254  prdsbas3  17645  prdsdsval2  17648  yonedalem4b  18443  gsum2d2lem  20180  coe1fzgsumdlem  22614  evl1gsumdlem  22667  ptcldmpt  23926  ptcnp  23934  cnmpt11  23975  cnmpt21  23983  cnmptk2  23998  prdsdsf  24679  prdsxmet  24681  ovolfiniun  25815  ovoliunlem3  25818  ovoliun  25819  ovoliun2  25820  ovoliunnul  25821  volfiniun  25861  voliun  25868  mbfsup  25978  mbflim  25982  itg2splitlem  26062  itg2split  26063  itg2cnlem1  26075  isibl2  26080  nfitg1  26087  nfitg  26088  cbvitg  26089  itgabs  26148  dvlipcn  26307  lhop2  26328  dvfsumabs  26336  dvfsumrlim  26344  itgparts  26360  itgsubstlem  26361  ulmss  26717  itgulm2  26729  lgamgulmlem2  27350  lgamgulmlem6  27354  lgamgulm2  27356  lgseisenlem2  27696  dchrisumlem3  27811  ltsval2  28006  nfseqs  28666  cnlnadjlem5  32666  dfimafnf  33223  2ndresdju  33236  deg1prod  34108  esumfzf  34694  voliune  34855  volfiniune  34856  bnj1534  35476  bnj1542  35480  bnj958  35563  bnj1000  35564  bnj1446  35668  bnj1447  35669  bnj1448  35670  bnj1466  35676  bnj1467  35677  bnj1519  35688  bnj1520  35689  bnj1529  35693  onvf1odlem2  35866  vonf1oonfo  35877  cvmcov  36007  rdgssun  38281  exrecfnlem  38282  finxpreclem2  38293  finxpreclem6  38299  poimirlem23  38541  poimirlem27  38545  itgabsnc  38587  riotaocN  40246  cdleme32d  41481  cdleme32f  41483  ltrniotaval  41618  cdlemksv2  41884  cdlemkuv2  41904  cdlemk36  41950  cdlemk38  41952  cdlemk19x  41980  cdlemk11t  41983  evl1gprodd  43147  mzpsubst  43738  aomclem8  44047  mnringmulrcld  45211  binomcxplemdvbinom  45322  binomcxplemdvsum  45324  binomcxplemnotnn0  45325  nfrelp  45917  permaxrep  45974  permaxsep  45975  evth2f  46001  fvelrnbf  46004  evthf  46013  rfcnpre3  46019  rfcnpre4  46020  rfcnnnub  46022  refsum2cnlem1  46023  allbutfiinf  46399  monoordxr  46461  monoord2xr  46463  caucvgbf  46468  cvgcaule  46470  fmul01  46561  fmuldfeqlem1  46563  fmuldfeq  46564  fmul01lt1lem1  46565  fmul01lt1lem2  46566  fmul01lt1  46567  cncfmptss  46568  mulc1cncfg  46570  expcnfg  46572  fprodabs2  46576  climmulf  46585  climexp  46586  climsuse  46589  climrecf  46590  climinff  46592  climaddf  46596  mullimc  46597  idlimc  46607  limcperiod  46609  neglimc  46626  addlimc  46627  0ellimcdiv  46628  fnlimfv  46642  climreclf  46643  fnlimcnv  46646  fnlimfvre  46653  fnlimfvre2  46656  fnlimf  46657  fnlimabslt  46658  climfveqf  46659  climmptf  46660  climeldmeqf  46662  limsupref  46664  limsupbnd1f  46665  climbddf  46666  climeqf  46667  limsuppnfd  46681  climinf2  46686  limsuppnf  46690  limsupubuz  46692  climinfmpt  46694  limsupmnf  46700  limsupequz  46702  limsupre2  46704  limsupmnfuz  46706  limsupre3  46712  limsupre3uz  46715  limsupreuz  46716  climuz  46723  lmbr3  46726  limsupgt  46757  liminfvalxr  46762  liminfreuz  46782  liminflt  46784  xlimpnfxnegmnf  46793  liminfpnfuz  46795  xlimmnf  46820  xlimpnf  46821  dfxlim2  46827  xlimpnfxnegmnf2  46837  cncfshift  46853  icccncfext  46866  cncficcgt0  46867  cncfiooicclem1  46872  dvnmul  46922  dvnprodlem1  46925  itgsubsticclem  46954  stoweidlem3  46982  stoweidlem23  47002  stoweidlem26  47005  stoweidlem28  47007  stoweidlem29  47008  stoweidlem31  47010  stoweidlem34  47013  stoweidlem36  47015  stoweidlem42  47021  stoweidlem48  47027  stoweidlem51  47030  stoweidlem52  47031  stoweidlem59  47038  wallispilem5  47048  stirlinglem4  47056  stirlinglem11  47063  stirlinglem12  47064  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  fourierdlem20  47106  fourierdlem31  47117  fourierdlem79  47164  fourierdlem89  47174  fourierdlem91  47176  fourierdlem112  47197  fourierdlem115  47200  fourierd  47201  fourierclimd  47202  etransclem2  47215  etransclem48  47261  sge0revalmpt  47357  sge0fsummpt  47369  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0iunmpt  47397  sge0xadd  47414  sge0fsummptf  47415  sge0gtfsumgt  47422  iundjiun  47439  meadjiun  47445  voliunsge0lem  47451  meaiunincf  47462  meaiuninc3  47464  omeiunle  47496  omeiunltfirp  47498  ovncvrrp  47543  vonioo  47661  vonicc  47664  vonn0ioo2  47669  vonn0icc2  47671  pimltmnf2f  47676  pimgtpnf2f  47684  pimltpnf2f  47691  pimgtmnf2  47693  pimdecfgtioc  47694  issmff  47713  smfpimltxrmptf  47737  smfpreimagtf  47747  smflim  47756  smfpimgtxr  47759  smfpimgtxrmptf  47763  smfmullem4  47773  smflim2  47785  smfpimcclem  47786  smfpimcc  47787  smfsup  47793  smfsupmpt  47794  smfsupxr  47795  smfinflem  47796  smfinf  47797  smflimsuplem2  47800  smflimsuplem5  47803  smflimsuplem7  47805  smflimsup  47807  smfliminf  47810  fsupdm  47821  smfsupdmmbllem  47823  finfdm  47825  smfinfdmmbllem  47827  nfafv  48175  nfsetrecs  50758