Theorem nffv 6877

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 6529	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2924	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5147	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6481	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2922	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2909   class class class wbr 5100  ℩cio 6475  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529

This theorem is referenced by:  nffvmpt1  6878  nffvd  6879  fvelimad  6934  dffn5f  6938  fvmptss  6988  fvmptex  6990  fvmptf  6997  fvmptnf  6998  eqfnfv2f  7015  ralrnmptw  7075  ralrnmpt  7077  dffo3f  7087  ffnfvf  7101  funiunfvf  7233  dff13f  7239  nfiso  7306  nfrdg  8385  rdgsucmptf  8399  rdgsucmptnf  8400  frsucmpt  8409  frsucmptn  8410  ttrclselem1  9680  ttrclselem2  9681  rankidb  9758  rankval4  9825  dfac8clem  9988  cardaleph  10045  hsmexlem2  10384  axcc2  10394  uniimadomf  10502  nfseq  14024  seqof2  14073  rlim2  15523  nfsum1  15717  nfsum  15718  sumeq2ii  15720  fsumrelem  15835  o1fsum  15841  nfcprod1  15938  nfcprod  15939  fprodefsum  16125  prdsbas3  17510  prdsdsval2  17513  yonedalem4b  18308  gsum2d2lem  20013  coe1fzgsumdlem  22363  evl1gsumdlem  22416  ptcldmpt  23671  ptcnp  23679  cnmpt11  23720  cnmpt21  23728  cnmptk2  23743  prdsdsf  24424  prdsxmet  24426  ovolfiniun  25560  ovoliunlem3  25563  ovoliun  25564  ovoliun2  25565  ovoliunnul  25566  volfiniun  25606  voliun  25613  mbfsup  25723  mbflim  25727  itg2splitlem  25807  itg2split  25808  itg2cnlem1  25820  isibl2  25825  nfitg1  25833  nfitg  25834  cbvitg  25835  itgabs  25894  dvlipcn  26053  lhop2  26074  dvfsumabs  26082  dvfsumrlim  26090  itgparts  26106  itgsubstlem  26107  ulmss  26457  itgulm2  26469  lgamgulmlem2  27091  lgamgulmlem6  27095  lgamgulm2  27097  lgseisenlem2  27437  dchrisumlem3  27552  ltsval2  27717  nfseqs  28377  cnlnadjlem5  32271  dfimafnf  32835  2ndresdju  32848  deg1prod  33776  esumfzf  34363  voliune  34523  volfiniune  34524  bnj1534  35145  bnj1542  35149  bnj958  35232  bnj1000  35233  bnj1446  35337  bnj1447  35338  bnj1448  35339  bnj1466  35345  bnj1467  35346  bnj1519  35357  bnj1520  35358  bnj1529  35362  rankval4b  35393  onvf1odlem2  35444  vonf1oonfo  35455  cvmcov  35610  rdgssun  37869  exrecfnlem  37870  finxpreclem2  37881  finxpreclem6  37887  poimirlem23  38139  poimirlem27  38143  itgabsnc  38185  riotaocN  39830  cdleme32d  41065  cdleme32f  41067  ltrniotaval  41202  cdlemksv2  41468  cdlemkuv2  41488  cdlemk36  41534  cdlemk38  41536  cdlemk19x  41564  cdlemk11t  41567  evl1gprodd  42731  mzpsubst  43326  aomclem8  43635  mnringmulrcld  44801  binomcxplemdvbinom  44926  binomcxplemdvsum  44928  binomcxplemnotnn0  44929  nfrelp  45522  permaxrep  45579  permaxsep  45580  evth2f  45592  fvelrnbf  45595  evthf  45604  rfcnpre3  45610  rfcnpre4  45611  rfcnnnub  45613  refsum2cnlem1  45614  allbutfiinf  45991  monoordxr  46053  monoord2xr  46055  caucvgbf  46060  cvgcaule  46062  fmul01  46153  fmuldfeqlem1  46155  fmuldfeq  46156  fmul01lt1lem1  46157  fmul01lt1lem2  46158  fmul01lt1  46159  cncfmptss  46160  mulc1cncfg  46162  expcnfg  46164  fprodabs2  46168  climmulf  46177  climexp  46178  climsuse  46181  climrecf  46182  climinff  46184  climaddf  46188  mullimc  46189  idlimc  46199  limcperiod  46201  neglimc  46218  addlimc  46219  0ellimcdiv  46220  fnlimfv  46234  climreclf  46235  fnlimcnv  46238  fnlimfvre  46245  fnlimfvre2  46248  fnlimf  46249  fnlimabslt  46250  climfveqf  46251  climmptf  46252  climeldmeqf  46254  limsupref  46256  limsupbnd1f  46257  climbddf  46258  climeqf  46259  limsuppnfd  46273  climinf2  46278  limsuppnf  46282  limsupubuz  46284  climinfmpt  46286  limsupmnf  46292  limsupequz  46294  limsupre2  46296  limsupmnfuz  46298  limsupre3  46304  limsupre3uz  46307  limsupreuz  46308  climuz  46315  lmbr3  46318  limsupgt  46349  liminfvalxr  46354  liminfreuz  46374  liminflt  46376  xlimpnfxnegmnf  46385  liminfpnfuz  46387  xlimmnf  46412  xlimpnf  46413  dfxlim2  46419  xlimpnfxnegmnf2  46429  cncfshift  46445  icccncfext  46458  cncficcgt0  46459  cncfiooicclem1  46464  dvnmul  46514  dvnprodlem1  46517  itgsubsticclem  46546  stoweidlem3  46574  stoweidlem23  46594  stoweidlem26  46597  stoweidlem28  46599  stoweidlem29  46600  stoweidlem31  46602  stoweidlem34  46605  stoweidlem36  46607  stoweidlem42  46613  stoweidlem48  46619  stoweidlem51  46622  stoweidlem52  46623  stoweidlem59  46630  wallispilem5  46640  stirlinglem4  46648  stirlinglem11  46655  stirlinglem12  46656  stirlinglem13  46657  stirlinglem14  46658  stirlinglem15  46659  fourierdlem20  46698  fourierdlem31  46709  fourierdlem79  46756  fourierdlem89  46766  fourierdlem91  46768  fourierdlem112  46789  fourierdlem115  46792  fourierd  46793  fourierclimd  46794  etransclem2  46807  etransclem48  46853  sge0revalmpt  46949  sge0fsummpt  46961  sge0iunmptlemfi  46984  sge0iunmptlemre  46986  sge0iunmpt  46989  sge0xadd  47006  sge0fsummptf  47007  sge0gtfsumgt  47014  iundjiun  47031  meadjiun  47037  voliunsge0lem  47043  meaiunincf  47054  meaiuninc3  47056  omeiunle  47088  omeiunltfirp  47090  ovncvrrp  47135  vonioo  47253  vonicc  47256  vonn0ioo2  47261  vonn0icc2  47263  pimltmnf2f  47268  pimgtpnf2f  47276  pimltpnf2f  47283  pimgtmnf2  47285  pimdecfgtioc  47286  issmff  47305  smfpimltxrmptf  47329  smfpreimagtf  47339  smflim  47348  smfpimgtxr  47351  smfpimgtxrmptf  47355  smfmullem4  47365  smflim2  47377  smfpimcclem  47378  smfpimcc  47379  smfsup  47385  smfsupmpt  47386  smfsupxr  47387  smfinflem  47388  smfinf  47389  smflimsuplem2  47392  smflimsuplem5  47395  smflimsuplem7  47397  smflimsup  47399  smfliminf  47402  fsupdm  47413  smfsupdmmbllem  47415  finfdm  47417  smfinfdmmbllem  47419  nfafv  47727  nfsetrecs  50304  setrec2fun  50310