Theorem nffv 6840

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 6496	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2903	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5121	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6448	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2901	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2888   class class class wbr 5074  ℩cio 6442  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496

This theorem is referenced by:  nffvmpt1  6841  nffvd  6842  fvelimad  6897  dffn5f  6901  fvmptss  6951  fvmptex  6953  fvmptf  6960  fvmptnf  6961  eqfnfv2f  6978  ralrnmptw  7038  ralrnmpt  7040  dffo3f  7050  ffnfvf  7064  funiunfvf  7196  dff13f  7202  nfiso  7269  nfrdg  8347  rdgsucmptf  8361  rdgsucmptnf  8362  frsucmpt  8371  frsucmptn  8372  ttrclselem1  9641  ttrclselem2  9642  rankidb  9719  rankval4  9786  dfac8clem  9949  cardaleph  10006  hsmexlem2  10345  axcc2  10355  uniimadomf  10463  nfseq  13968  seqof2  14017  rlim2  15453  nfsum1  15647  nfsum  15648  sumeq2ii  15650  fsumrelem  15765  o1fsum  15771  nfcprod1  15868  nfcprod  15869  fprodefsum  16055  prdsbas3  17439  prdsdsval2  17442  yonedalem4b  18237  gsum2d2lem  19942  coe1fzgsumdlem  22292  evl1gsumdlem  22345  ptcldmpt  23600  ptcnp  23608  cnmpt11  23649  cnmpt21  23657  cnmptk2  23672  prdsdsf  24353  prdsxmet  24355  ovolfiniun  25489  ovoliunlem3  25492  ovoliun  25493  ovoliun2  25494  ovoliunnul  25495  volfiniun  25535  voliun  25542  mbfsup  25652  mbflim  25656  itg2splitlem  25736  itg2split  25737  itg2cnlem1  25749  isibl2  25754  nfitg1  25762  nfitg  25763  cbvitg  25764  itgabs  25823  dvlipcn  25982  lhop2  26003  dvfsumabs  26011  dvfsumrlim  26019  itgparts  26035  itgsubstlem  26036  ulmss  26383  itgulm2  26395  lgamgulmlem2  27014  lgamgulmlem6  27018  lgamgulm2  27020  lgseisenlem2  27360  dchrisumlem3  27475  ltsval2  27640  nfseqs  28299  cnlnadjlem5  32162  dfimafnf  32730  2ndresdju  32743  deg1prod  33676  esumfzf  34263  voliune  34423  volfiniune  34424  bnj1534  35048  bnj1542  35052  bnj958  35135  bnj1000  35136  bnj1446  35240  bnj1447  35241  bnj1448  35242  bnj1466  35248  bnj1467  35249  bnj1519  35260  bnj1520  35261  bnj1529  35265  rankval4b  35294  onvf1odlem2  35345  cvmcov  35504  rdgssun  37753  exrecfnlem  37754  finxpreclem2  37765  finxpreclem6  37771  poimirlem23  38023  poimirlem27  38027  itgabsnc  38069  riotaocN  39714  cdleme32d  40949  cdleme32f  40951  ltrniotaval  41086  cdlemksv2  41352  cdlemkuv2  41372  cdlemk36  41418  cdlemk38  41420  cdlemk19x  41448  cdlemk11t  41451  evl1gprodd  42615  mzpsubst  43210  aomclem8  43519  mnringmulrcld  44685  binomcxplemdvbinom  44810  binomcxplemdvsum  44812  binomcxplemnotnn0  44813  nfrelp  45406  permaxrep  45463  permaxsep  45464  evth2f  45476  fvelrnbf  45479  evthf  45488  rfcnpre3  45494  rfcnpre4  45495  rfcnnnub  45497  refsum2cnlem1  45498  allbutfiinf  45875  monoordxr  45937  monoord2xr  45939  caucvgbf  45944  cvgcaule  45946  fmul01  46037  fmuldfeqlem1  46039  fmuldfeq  46040  fmul01lt1lem1  46041  fmul01lt1lem2  46042  fmul01lt1  46043  cncfmptss  46044  mulc1cncfg  46046  expcnfg  46048  fprodabs2  46052  climmulf  46061  climexp  46062  climsuse  46065  climrecf  46066  climinff  46068  climaddf  46072  mullimc  46073  idlimc  46083  limcperiod  46085  neglimc  46102  addlimc  46103  0ellimcdiv  46104  fnlimfv  46118  climreclf  46119  fnlimcnv  46122  fnlimfvre  46129  fnlimfvre2  46132  fnlimf  46133  fnlimabslt  46134  climfveqf  46135  climmptf  46136  climeldmeqf  46138  limsupref  46140  limsupbnd1f  46141  climbddf  46142  climeqf  46143  limsuppnfd  46157  climinf2  46162  limsuppnf  46166  limsupubuz  46168  climinfmpt  46170  limsupmnf  46176  limsupequz  46178  limsupre2  46180  limsupmnfuz  46182  limsupre3  46188  limsupre3uz  46191  limsupreuz  46192  climuz  46199  lmbr3  46202  limsupgt  46233  liminfvalxr  46238  liminfreuz  46258  liminflt  46260  xlimpnfxnegmnf  46269  liminfpnfuz  46271  xlimmnf  46296  xlimpnf  46297  dfxlim2  46303  xlimpnfxnegmnf2  46313  cncfshift  46329  icccncfext  46342  cncficcgt0  46343  cncfiooicclem1  46348  dvnmul  46398  dvnprodlem1  46401  itgsubsticclem  46430  stoweidlem3  46458  stoweidlem23  46478  stoweidlem26  46481  stoweidlem28  46483  stoweidlem29  46484  stoweidlem31  46486  stoweidlem34  46489  stoweidlem36  46491  stoweidlem42  46497  stoweidlem48  46503  stoweidlem51  46506  stoweidlem52  46507  stoweidlem59  46514  wallispilem5  46524  stirlinglem4  46532  stirlinglem11  46539  stirlinglem12  46540  stirlinglem13  46541  stirlinglem14  46542  stirlinglem15  46543  fourierdlem20  46582  fourierdlem31  46593  fourierdlem79  46640  fourierdlem89  46650  fourierdlem91  46652  fourierdlem112  46673  fourierdlem115  46676  fourierd  46677  fourierclimd  46678  etransclem2  46691  etransclem48  46737  sge0revalmpt  46833  sge0fsummpt  46845  sge0iunmptlemfi  46868  sge0iunmptlemre  46870  sge0iunmpt  46873  sge0xadd  46890  sge0fsummptf  46891  sge0gtfsumgt  46898  iundjiun  46915  meadjiun  46921  voliunsge0lem  46927  meaiunincf  46938  meaiuninc3  46940  omeiunle  46972  omeiunltfirp  46974  ovncvrrp  47019  vonioo  47137  vonicc  47140  vonn0ioo2  47145  vonn0icc2  47147  pimltmnf2f  47152  pimgtpnf2f  47160  pimltpnf2f  47167  pimgtmnf2  47169  pimdecfgtioc  47170  issmff  47189  smfpimltxrmptf  47213  smfpreimagtf  47223  smflim  47232  smfpimgtxr  47235  smfpimgtxrmptf  47239  smfmullem4  47249  smflim2  47261  smfpimcclem  47262  smfpimcc  47263  smfsup  47269  smfsupmpt  47270  smfsupxr  47271  smfinflem  47272  smfinf  47273  smflimsuplem2  47276  smflimsuplem5  47279  smflimsuplem7  47281  smflimsup  47283  smfliminf  47286  fsupdm  47297  smfsupdmmbllem  47299  finfdm  47301  smfinfdmmbllem  47303  nfafv  47611  nfsetrecs  50188  setrec2fun  50194