Theorem nffv 6837

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

Syntax hints:  Ⅎwnfc 2886   class class class wbr 5072  ℩cio 6439  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493

This theorem is referenced by:  nffvmpt1  6838  nffvd  6839  fvelimad  6894  dffn5f  6898  fvmptss  6948  fvmptex  6950  fvmptf  6957  fvmptnf  6958  eqfnfv2f  6975  ralrnmptw  7035  ralrnmpt  7037  dffo3f  7047  ffnfvf  7061  funiunfvf  7193  dff13f  7199  nfiso  7266  nfrdg  8343  rdgsucmptf  8357  rdgsucmptnf  8358  frsucmpt  8367  frsucmptn  8368  ttrclselem1  9637  ttrclselem2  9638  rankidb  9715  rankval4  9782  dfac8clem  9945  cardaleph  10002  hsmexlem2  10340  axcc2  10350  uniimadomf  10458  nfseq  13964  seqof2  14013  rlim2  15449  nfsum1  15643  nfsum  15644  sumeq2ii  15646  fsumrelem  15761  o1fsum  15767  nfcprod1  15864  nfcprod  15865  fprodefsum  16051  prdsbas3  17435  prdsdsval2  17438  yonedalem4b  18233  gsum2d2lem  19939  coe1fzgsumdlem  22289  evl1gsumdlem  22342  ptcldmpt  23597  ptcnp  23605  cnmpt11  23646  cnmpt21  23654  cnmptk2  23669  prdsdsf  24350  prdsxmet  24352  ovolfiniun  25486  ovoliunlem3  25489  ovoliun  25490  ovoliun2  25491  ovoliunnul  25492  volfiniun  25532  voliun  25539  mbfsup  25649  mbflim  25653  itg2splitlem  25733  itg2split  25734  itg2cnlem1  25746  isibl2  25751  nfitg1  25759  nfitg  25760  cbvitg  25761  itgabs  25820  dvlipcn  25979  lhop2  26000  dvfsumabs  26008  dvfsumrlim  26016  itgparts  26032  itgsubstlem  26033  ulmss  26380  itgulm2  26392  lgamgulmlem2  27011  lgamgulmlem6  27015  lgamgulm2  27017  lgseisenlem2  27357  dchrisumlem3  27472  ltsval2  27638  nfseqs  28297  cnlnadjlem5  32160  dfimafnf  32728  2ndresdju  32741  deg1prod  33666  esumfzf  34253  voliune  34413  volfiniune  34414  bnj1534  35035  bnj1542  35039  bnj958  35122  bnj1000  35123  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1466  35235  bnj1467  35236  bnj1519  35247  bnj1520  35248  bnj1529  35252  rankval4b  35281  onvf1odlem2  35332  cvmcov  35491  rdgssun  37740  exrecfnlem  37741  finxpreclem2  37752  finxpreclem6  37758  poimirlem23  38010  poimirlem27  38014  itgabsnc  38056  riotaocN  39701  cdleme32d  40936  cdleme32f  40938  ltrniotaval  41073  cdlemksv2  41339  cdlemkuv2  41359  cdlemk36  41405  cdlemk38  41407  cdlemk19x  41435  cdlemk11t  41438  evl1gprodd  42602  mzpsubst  43197  aomclem8  43506  mnringmulrcld  44672  binomcxplemdvbinom  44797  binomcxplemdvsum  44799  binomcxplemnotnn0  44800  nfrelp  45393  permaxrep  45450  permaxsep  45451  evth2f  45463  fvelrnbf  45466  evthf  45475  rfcnpre3  45481  rfcnpre4  45482  rfcnnnub  45484  refsum2cnlem1  45485  allbutfiinf  45863  monoordxr  45925  monoord2xr  45927  caucvgbf  45932  cvgcaule  45934  fmul01  46025  fmuldfeqlem1  46027  fmuldfeq  46028  fmul01lt1lem1  46029  fmul01lt1lem2  46030  fmul01lt1  46031  cncfmptss  46032  mulc1cncfg  46034  expcnfg  46036  fprodabs2  46040  climmulf  46049  climexp  46050  climsuse  46053  climrecf  46054  climinff  46056  climaddf  46060  mullimc  46061  idlimc  46071  limcperiod  46073  neglimc  46090  addlimc  46091  0ellimcdiv  46092  fnlimfv  46106  climreclf  46107  fnlimcnv  46110  fnlimfvre  46117  fnlimfvre2  46120  fnlimf  46121  fnlimabslt  46122  climfveqf  46123  climmptf  46124  climeldmeqf  46126  limsupref  46128  limsupbnd1f  46129  climbddf  46130  climeqf  46131  limsuppnfd  46145  climinf2  46150  limsuppnf  46154  limsupubuz  46156  climinfmpt  46158  limsupmnf  46164  limsupequz  46166  limsupre2  46168  limsupmnfuz  46170  limsupre3  46176  limsupre3uz  46179  limsupreuz  46180  climuz  46187  lmbr3  46190  limsupgt  46221  liminfvalxr  46226  liminfreuz  46246  liminflt  46248  xlimpnfxnegmnf  46257  liminfpnfuz  46259  xlimmnf  46284  xlimpnf  46285  dfxlim2  46291  xlimpnfxnegmnf2  46301  cncfshift  46317  icccncfext  46330  cncficcgt0  46331  cncfiooicclem1  46336  dvnmul  46386  dvnprodlem1  46389  itgsubsticclem  46418  stoweidlem3  46446  stoweidlem23  46466  stoweidlem26  46469  stoweidlem28  46471  stoweidlem29  46472  stoweidlem31  46474  stoweidlem34  46477  stoweidlem36  46479  stoweidlem42  46485  stoweidlem48  46491  stoweidlem51  46494  stoweidlem52  46495  stoweidlem59  46502  wallispilem5  46512  stirlinglem4  46520  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  fourierdlem20  46570  fourierdlem31  46581  fourierdlem79  46628  fourierdlem89  46638  fourierdlem91  46640  fourierdlem112  46661  fourierdlem115  46664  fourierd  46665  fourierclimd  46666  etransclem2  46679  etransclem48  46725  sge0revalmpt  46821  sge0fsummpt  46833  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0xadd  46878  sge0fsummptf  46879  sge0gtfsumgt  46886  iundjiun  46903  meadjiun  46909  voliunsge0lem  46915  meaiunincf  46926  meaiuninc3  46928  omeiunle  46960  omeiunltfirp  46962  ovncvrrp  47007  vonioo  47125  vonicc  47128  vonn0ioo2  47133  vonn0icc2  47135  pimltmnf2f  47140  pimgtpnf2f  47148  pimltpnf2f  47155  pimgtmnf2  47157  pimdecfgtioc  47158  issmff  47177  smfpimltxrmptf  47201  smfpreimagtf  47211  smflim  47220  smfpimgtxr  47223  smfpimgtxrmptf  47227  smfmullem4  47237  smflim2  47249  smfpimcclem  47250  smfpimcc  47251  smfsup  47257  smfsupmpt  47258  smfsupxr  47259  smfinflem  47260  smfinf  47261  smflimsuplem2  47264  smflimsuplem5  47267  smflimsuplem7  47269  smflimsup  47271  smfliminf  47274  fsupdm  47285  smfsupdmmbllem  47287  finfdm  47289  smfinfdmmbllem  47291  nfafv  47599  nfsetrecs  50176  setrec2fun  50182