Theorem nffv 6885

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

Syntax hints:  Ⅎwnfc 2883   class class class wbr 5119  ℩cio 6481  ‘cfv 6530

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538

This theorem is referenced by:  nffvmpt1  6886  nffvd  6887  fvelimad  6945  dffn5f  6949  fvmptss  6997  fvmptex  6999  fvmptf  7006  fvmptnf  7007  eqfnfv2f  7024  ralrnmptw  7083  ralrnmpt  7085  dffo3f  7095  ffnfvf  7109  funiunfvf  7240  dff13f  7247  nfiso  7314  nfwrecsOLD  8314  nfrdg  8426  rdgsucmptf  8440  rdgsucmptnf  8441  frsucmpt  8450  frsucmptn  8451  ttrclselem1  9737  ttrclselem2  9738  rankidb  9812  rankval4  9879  dfac8clem  10044  cardaleph  10101  hsmexlem2  10439  axcc2  10449  uniimadomf  10557  nfseq  14027  seqof2  14076  rlim2  15510  nfsum1  15704  nfsum  15705  sumeq2ii  15707  fsumrelem  15821  o1fsum  15827  nfcprod1  15922  nfcprod  15923  fprodefsum  16109  prdsbas3  17493  prdsdsval2  17496  yonedalem4b  18286  gsum2d2lem  19952  coe1fzgsumdlem  22239  evl1gsumdlem  22292  ptcldmpt  23550  ptcnp  23558  cnmpt11  23599  cnmpt21  23607  cnmptk2  23622  prdsdsf  24304  prdsxmet  24306  ovolfiniun  25452  ovoliunlem3  25455  ovoliun  25456  ovoliun2  25457  ovoliunnul  25458  volfiniun  25498  voliun  25505  mbfsup  25615  mbflim  25619  itg2splitlem  25699  itg2split  25700  itg2cnlem1  25712  isibl2  25717  nfitg1  25725  nfitg  25726  cbvitg  25727  itgabs  25786  dvlipcn  25949  lhop2  25970  dvfsumabs  25979  dvfsumrlim  25988  itgparts  26004  itgsubstlem  26005  ulmss  26356  itgulm2  26368  lgamgulmlem2  26990  lgamgulmlem6  26994  lgamgulm2  26996  lgseisenlem2  27337  dchrisumlem3  27452  sltval2  27618  nfseqs  28210  cnlnadjlem5  31998  dfimafnf  32560  2ndresdju  32573  esumfzf  34046  voliune  34206  volfiniune  34207  bnj1534  34830  bnj1542  34834  bnj958  34917  bnj1000  34918  bnj1446  35022  bnj1447  35023  bnj1448  35024  bnj1466  35030  bnj1467  35031  bnj1519  35042  bnj1520  35043  bnj1529  35047  cvmcov  35231  rdgssun  37342  exrecfnlem  37343  finxpreclem2  37354  finxpreclem6  37360  poimirlem23  37613  poimirlem27  37617  itgabsnc  37659  riotaocN  39173  cdleme32d  40409  cdleme32f  40411  ltrniotaval  40546  cdlemksv2  40812  cdlemkuv2  40832  cdlemk36  40878  cdlemk38  40880  cdlemk19x  40908  cdlemk11t  40911  evl1gprodd  42076  mzpsubst  42718  aomclem8  43032  mnringmulrcld  44200  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  nfrelp  44922  permaxrep  44979  permaxsep  44980  evth2f  44987  fvelrnbf  44990  evthf  44999  rfcnpre3  45005  rfcnpre4  45006  rfcnnnub  45008  refsum2cnlem1  45009  allbutfiinf  45395  monoordxr  45457  monoord2xr  45459  caucvgbf  45464  cvgcaule  45466  fmul01  45557  fmuldfeqlem1  45559  fmuldfeq  45560  fmul01lt1lem1  45561  fmul01lt1lem2  45562  fmul01lt1  45563  cncfmptss  45564  mulc1cncfg  45566  expcnfg  45568  fprodabs2  45572  climmulf  45581  climexp  45582  climsuse  45585  climrecf  45586  climinff  45588  climaddf  45592  mullimc  45593  idlimc  45603  limcperiod  45605  neglimc  45624  addlimc  45625  0ellimcdiv  45626  fnlimfv  45640  climreclf  45641  fnlimcnv  45644  fnlimfvre  45651  fnlimfvre2  45654  fnlimf  45655  fnlimabslt  45656  climfveqf  45657  climmptf  45658  climeldmeqf  45660  limsupref  45662  limsupbnd1f  45663  climbddf  45664  climeqf  45665  limsuppnfd  45679  climinf2  45684  limsuppnf  45688  limsupubuz  45690  climinfmpt  45692  limsupmnf  45698  limsupequz  45700  limsupre2  45702  limsupmnfuz  45704  limsupre3  45710  limsupre3uz  45713  limsupreuz  45714  climuz  45721  lmbr3  45724  limsupgt  45755  liminfvalxr  45760  liminfreuz  45780  liminflt  45782  xlimpnfxnegmnf  45791  liminfpnfuz  45793  xlimmnf  45818  xlimpnf  45819  dfxlim2  45825  xlimpnfxnegmnf2  45835  cncfshift  45851  icccncfext  45864  cncficcgt0  45865  cncfiooicclem1  45870  dvnmul  45920  dvnprodlem1  45923  itgsubsticclem  45952  stoweidlem3  45980  stoweidlem23  46000  stoweidlem26  46003  stoweidlem28  46005  stoweidlem29  46006  stoweidlem31  46008  stoweidlem34  46011  stoweidlem36  46013  stoweidlem42  46019  stoweidlem48  46025  stoweidlem51  46028  stoweidlem52  46029  stoweidlem59  46036  wallispilem5  46046  stirlinglem4  46054  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  fourierdlem20  46104  fourierdlem31  46115  fourierdlem79  46162  fourierdlem89  46172  fourierdlem91  46174  fourierdlem112  46195  fourierdlem115  46198  fourierd  46199  fourierclimd  46200  etransclem2  46213  etransclem48  46259  sge0revalmpt  46355  sge0fsummpt  46367  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0xadd  46412  sge0fsummptf  46413  sge0gtfsumgt  46420  iundjiun  46437  meadjiun  46443  voliunsge0lem  46449  meaiunincf  46460  meaiuninc3  46462  omeiunle  46494  omeiunltfirp  46496  ovncvrrp  46541  vonioo  46659  vonicc  46662  vonn0ioo2  46667  vonn0icc2  46669  pimltmnf2f  46674  pimgtpnf2f  46682  pimltpnf2f  46689  pimgtmnf2  46691  pimdecfgtioc  46692  issmff  46711  smfpimltxrmptf  46735  smfpreimagtf  46745  smflim  46754  smfpimgtxr  46757  smfpimgtxrmptf  46761  smfmullem4  46771  smflim2  46783  smfpimcclem  46784  smfpimcc  46785  smfsup  46791  smfsupmpt  46792  smfsupxr  46793  smfinflem  46794  smfinf  46795  smflimsuplem2  46798  smflimsuplem5  46801  smflimsuplem7  46803  smflimsup  46805  smfliminf  46808  fsupdm  46819  smfsupdmmbllem  46821  finfdm  46823  smfinfdmmbllem  46825  nfafv  47113  nfsetrecs  49498  setrec2fun  49504