Theorem nffv 6842

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

Syntax hints:  Ⅎwnfc 2881   class class class wbr 5096  ℩cio 6444  ‘cfv 6490

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498

This theorem is referenced by:  nffvmpt1  6843  nffvd  6844  fvelimad  6899  dffn5f  6903  fvmptss  6951  fvmptex  6953  fvmptf  6960  fvmptnf  6961  eqfnfv2f  6978  ralrnmptw  7037  ralrnmpt  7039  dffo3f  7049  ffnfvf  7063  funiunfvf  7193  dff13f  7199  nfiso  7266  nfrdg  8343  rdgsucmptf  8357  rdgsucmptnf  8358  frsucmpt  8367  frsucmptn  8368  ttrclselem1  9632  ttrclselem2  9633  rankidb  9710  rankval4  9777  dfac8clem  9940  cardaleph  9997  hsmexlem2  10335  axcc2  10345  uniimadomf  10453  nfseq  13932  seqof2  13981  rlim2  15417  nfsum1  15611  nfsum  15612  sumeq2ii  15614  fsumrelem  15728  o1fsum  15734  nfcprod1  15829  nfcprod  15830  fprodefsum  16016  prdsbas3  17399  prdsdsval2  17402  yonedalem4b  18197  gsum2d2lem  19900  coe1fzgsumdlem  22245  evl1gsumdlem  22298  ptcldmpt  23556  ptcnp  23564  cnmpt11  23605  cnmpt21  23613  cnmptk2  23628  prdsdsf  24309  prdsxmet  24311  ovolfiniun  25456  ovoliunlem3  25459  ovoliun  25460  ovoliun2  25461  ovoliunnul  25462  volfiniun  25502  voliun  25509  mbfsup  25619  mbflim  25623  itg2splitlem  25703  itg2split  25704  itg2cnlem1  25716  isibl2  25721  nfitg1  25729  nfitg  25730  cbvitg  25731  itgabs  25790  dvlipcn  25953  lhop2  25974  dvfsumabs  25983  dvfsumrlim  25992  itgparts  26008  itgsubstlem  26009  ulmss  26360  itgulm2  26372  lgamgulmlem2  26994  lgamgulmlem6  26998  lgamgulm2  27000  lgseisenlem2  27341  dchrisumlem3  27456  sltval2  27622  nfseqs  28248  cnlnadjlem5  32095  dfimafnf  32663  2ndresdju  32676  deg1prod  33613  esumfzf  34175  voliune  34335  volfiniune  34336  bnj1534  34958  bnj1542  34962  bnj958  35045  bnj1000  35046  bnj1446  35150  bnj1447  35151  bnj1448  35152  bnj1466  35158  bnj1467  35159  bnj1519  35170  bnj1520  35171  bnj1529  35175  rankval4b  35205  onvf1odlem2  35247  cvmcov  35406  rdgssun  37522  exrecfnlem  37523  finxpreclem2  37534  finxpreclem6  37540  poimirlem23  37783  poimirlem27  37787  itgabsnc  37829  riotaocN  39408  cdleme32d  40643  cdleme32f  40645  ltrniotaval  40780  cdlemksv2  41046  cdlemkuv2  41066  cdlemk36  41112  cdlemk38  41114  cdlemk19x  41142  cdlemk11t  41145  evl1gprodd  42310  mzpsubst  42932  aomclem8  43245  mnringmulrcld  44411  binomcxplemdvbinom  44536  binomcxplemdvsum  44538  binomcxplemnotnn0  44539  nfrelp  45132  permaxrep  45189  permaxsep  45190  evth2f  45202  fvelrnbf  45205  evthf  45214  rfcnpre3  45220  rfcnpre4  45221  rfcnnnub  45223  refsum2cnlem1  45224  allbutfiinf  45606  monoordxr  45668  monoord2xr  45670  caucvgbf  45675  cvgcaule  45677  fmul01  45768  fmuldfeqlem1  45770  fmuldfeq  45771  fmul01lt1lem1  45772  fmul01lt1lem2  45773  fmul01lt1  45774  cncfmptss  45775  mulc1cncfg  45777  expcnfg  45779  fprodabs2  45783  climmulf  45792  climexp  45793  climsuse  45796  climrecf  45797  climinff  45799  climaddf  45803  mullimc  45804  idlimc  45814  limcperiod  45816  neglimc  45833  addlimc  45834  0ellimcdiv  45835  fnlimfv  45849  climreclf  45850  fnlimcnv  45853  fnlimfvre  45860  fnlimfvre2  45863  fnlimf  45864  fnlimabslt  45865  climfveqf  45866  climmptf  45867  climeldmeqf  45869  limsupref  45871  limsupbnd1f  45872  climbddf  45873  climeqf  45874  limsuppnfd  45888  climinf2  45893  limsuppnf  45897  limsupubuz  45899  climinfmpt  45901  limsupmnf  45907  limsupequz  45909  limsupre2  45911  limsupmnfuz  45913  limsupre3  45919  limsupre3uz  45922  limsupreuz  45923  climuz  45930  lmbr3  45933  limsupgt  45964  liminfvalxr  45969  liminfreuz  45989  liminflt  45991  xlimpnfxnegmnf  46000  liminfpnfuz  46002  xlimmnf  46027  xlimpnf  46028  dfxlim2  46034  xlimpnfxnegmnf2  46044  cncfshift  46060  icccncfext  46073  cncficcgt0  46074  cncfiooicclem1  46079  dvnmul  46129  dvnprodlem1  46132  itgsubsticclem  46161  stoweidlem3  46189  stoweidlem23  46209  stoweidlem26  46212  stoweidlem28  46214  stoweidlem29  46215  stoweidlem31  46217  stoweidlem34  46220  stoweidlem36  46222  stoweidlem42  46228  stoweidlem48  46234  stoweidlem51  46237  stoweidlem52  46238  stoweidlem59  46245  wallispilem5  46255  stirlinglem4  46263  stirlinglem11  46270  stirlinglem12  46271  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  fourierdlem20  46313  fourierdlem31  46324  fourierdlem79  46371  fourierdlem89  46381  fourierdlem91  46383  fourierdlem112  46404  fourierdlem115  46407  fourierd  46408  fourierclimd  46409  etransclem2  46422  etransclem48  46468  sge0revalmpt  46564  sge0fsummpt  46576  sge0iunmptlemfi  46599  sge0iunmptlemre  46601  sge0iunmpt  46604  sge0xadd  46621  sge0fsummptf  46622  sge0gtfsumgt  46629  iundjiun  46646  meadjiun  46652  voliunsge0lem  46658  meaiunincf  46669  meaiuninc3  46671  omeiunle  46703  omeiunltfirp  46705  ovncvrrp  46750  vonioo  46868  vonicc  46871  vonn0ioo2  46876  vonn0icc2  46878  pimltmnf2f  46883  pimgtpnf2f  46891  pimltpnf2f  46898  pimgtmnf2  46900  pimdecfgtioc  46901  issmff  46920  smfpimltxrmptf  46944  smfpreimagtf  46954  smflim  46963  smfpimgtxr  46966  smfpimgtxrmptf  46970  smfmullem4  46980  smflim2  46992  smfpimcclem  46993  smfpimcc  46994  smfsup  47000  smfsupmpt  47001  smfsupxr  47002  smfinflem  47003  smfinf  47004  smflimsuplem2  47007  smflimsuplem5  47010  smflimsuplem7  47012  smflimsup  47014  smfliminf  47017  fsupdm  47028  smfsupdmmbllem  47030  finfdm  47032  smfinfdmmbllem  47034  nfafv  47324  nfsetrecs  49873  setrec2fun  49879