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 6490	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2891	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5139	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6442	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2876   class class class wbr 5092  ℩cio 6436  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490

This theorem is referenced by:  nffvmpt1  6833  nffvd  6834  fvelimad  6890  dffn5f  6894  fvmptss  6942  fvmptex  6944  fvmptf  6951  fvmptnf  6952  eqfnfv2f  6969  ralrnmptw  7028  ralrnmpt  7030  dffo3f  7040  ffnfvf  7054  funiunfvf  7185  dff13f  7192  nfiso  7259  nfrdg  8336  rdgsucmptf  8350  rdgsucmptnf  8351  frsucmpt  8360  frsucmptn  8361  ttrclselem1  9621  ttrclselem2  9622  rankidb  9696  rankval4  9763  dfac8clem  9926  cardaleph  9983  hsmexlem2  10321  axcc2  10331  uniimadomf  10439  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  19852  coe1fzgsumdlem  22188  evl1gsumdlem  22241  ptcldmpt  23499  ptcnp  23507  cnmpt11  23548  cnmpt21  23556  cnmptk2  23571  prdsdsf  24253  prdsxmet  24255  ovolfiniun  25400  ovoliunlem3  25403  ovoliun  25404  ovoliun2  25405  ovoliunnul  25406  volfiniun  25446  voliun  25453  mbfsup  25563  mbflim  25567  itg2splitlem  25647  itg2split  25648  itg2cnlem1  25660  isibl2  25665  nfitg1  25673  nfitg  25674  cbvitg  25675  itgabs  25734  dvlipcn  25897  lhop2  25918  dvfsumabs  25927  dvfsumrlim  25936  itgparts  25952  itgsubstlem  25953  ulmss  26304  itgulm2  26316  lgamgulmlem2  26938  lgamgulmlem6  26942  lgamgulm2  26944  lgseisenlem2  27285  dchrisumlem3  27400  sltval2  27566  nfseqs  28186  cnlnadjlem5  32015  dfimafnf  32579  2ndresdju  32592  esumfzf  34036  voliune  34196  volfiniune  34197  bnj1534  34820  bnj1542  34824  bnj958  34907  bnj1000  34908  bnj1446  35012  bnj1447  35013  bnj1448  35014  bnj1466  35020  bnj1467  35021  bnj1519  35032  bnj1520  35033  bnj1529  35037  onvf1odlem2  35077  cvmcov  35236  rdgssun  37352  exrecfnlem  37353  finxpreclem2  37364  finxpreclem6  37370  poimirlem23  37623  poimirlem27  37627  itgabsnc  37669  riotaocN  39188  cdleme32d  40423  cdleme32f  40425  ltrniotaval  40560  cdlemksv2  40826  cdlemkuv2  40846  cdlemk36  40892  cdlemk38  40894  cdlemk19x  40922  cdlemk11t  40925  evl1gprodd  42090  mzpsubst  42721  aomclem8  43034  mnringmulrcld  44201  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  nfrelp  44923  permaxrep  44980  permaxsep  44981  evth2f  44993  fvelrnbf  44996  evthf  45005  rfcnpre3  45011  rfcnpre4  45012  rfcnnnub  45014  refsum2cnlem1  45015  allbutfiinf  45399  monoordxr  45461  monoord2xr  45463  caucvgbf  45468  cvgcaule  45470  fmul01  45561  fmuldfeqlem1  45563  fmuldfeq  45564  fmul01lt1lem1  45565  fmul01lt1lem2  45566  fmul01lt1  45567  cncfmptss  45568  mulc1cncfg  45570  expcnfg  45572  fprodabs2  45576  climmulf  45585  climexp  45586  climsuse  45589  climrecf  45590  climinff  45592  climaddf  45596  mullimc  45597  idlimc  45607  limcperiod  45609  neglimc  45628  addlimc  45629  0ellimcdiv  45630  fnlimfv  45644  climreclf  45645  fnlimcnv  45648  fnlimfvre  45655  fnlimfvre2  45658  fnlimf  45659  fnlimabslt  45660  climfveqf  45661  climmptf  45662  climeldmeqf  45664  limsupref  45666  limsupbnd1f  45667  climbddf  45668  climeqf  45669  limsuppnfd  45683  climinf2  45688  limsuppnf  45692  limsupubuz  45694  climinfmpt  45696  limsupmnf  45702  limsupequz  45704  limsupre2  45706  limsupmnfuz  45708  limsupre3  45714  limsupre3uz  45717  limsupreuz  45718  climuz  45725  lmbr3  45728  limsupgt  45759  liminfvalxr  45764  liminfreuz  45784  liminflt  45786  xlimpnfxnegmnf  45795  liminfpnfuz  45797  xlimmnf  45822  xlimpnf  45823  dfxlim2  45829  xlimpnfxnegmnf2  45839  cncfshift  45855  icccncfext  45868  cncficcgt0  45869  cncfiooicclem1  45874  dvnmul  45924  dvnprodlem1  45927  itgsubsticclem  45956  stoweidlem3  45984  stoweidlem23  46004  stoweidlem26  46007  stoweidlem28  46009  stoweidlem29  46010  stoweidlem31  46012  stoweidlem34  46015  stoweidlem36  46017  stoweidlem42  46023  stoweidlem48  46029  stoweidlem51  46032  stoweidlem52  46033  stoweidlem59  46040  wallispilem5  46050  stirlinglem4  46058  stirlinglem11  46065  stirlinglem12  46066  stirlinglem13  46067  stirlinglem14  46068  stirlinglem15  46069  fourierdlem20  46108  fourierdlem31  46119  fourierdlem79  46166  fourierdlem89  46176  fourierdlem91  46178  fourierdlem112  46199  fourierdlem115  46202  fourierd  46203  fourierclimd  46204  etransclem2  46217  etransclem48  46263  sge0revalmpt  46359  sge0fsummpt  46371  sge0iunmptlemfi  46394  sge0iunmptlemre  46396  sge0iunmpt  46399  sge0xadd  46416  sge0fsummptf  46417  sge0gtfsumgt  46424  iundjiun  46441  meadjiun  46447  voliunsge0lem  46453  meaiunincf  46464  meaiuninc3  46466  omeiunle  46498  omeiunltfirp  46500  ovncvrrp  46545  vonioo  46663  vonicc  46666  vonn0ioo2  46671  vonn0icc2  46673  pimltmnf2f  46678  pimgtpnf2f  46686  pimltpnf2f  46693  pimgtmnf2  46695  pimdecfgtioc  46696  issmff  46715  smfpimltxrmptf  46739  smfpreimagtf  46749  smflim  46758  smfpimgtxr  46761  smfpimgtxrmptf  46765  smfmullem4  46775  smflim2  46787  smfpimcclem  46788  smfpimcc  46789  smfsup  46795  smfsupmpt  46796  smfsupxr  46797  smfinflem  46798  smfinf  46799  smflimsuplem2  46802  smflimsuplem5  46805  smflimsuplem7  46807  smflimsup  46809  smfliminf  46812  fsupdm  46823  smfsupdmmbllem  46825  finfdm  46827  smfinfdmmbllem  46829  nfafv  47120  nfsetrecs  49671  setrec2fun  49677