Theorem nffv 6871

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 6522	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2892	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5157	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6471	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2890	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2877   class class class wbr 5110  ℩cio 6465  ‘cfv 6514

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522

This theorem is referenced by:  nffvmpt1  6872  nffvd  6873  fvelimad  6931  dffn5f  6935  fvmptss  6983  fvmptex  6985  fvmptf  6992  fvmptnf  6993  eqfnfv2f  7010  ralrnmptw  7069  ralrnmpt  7071  dffo3f  7081  ffnfvf  7095  funiunfvf  7226  dff13f  7233  nfiso  7300  nfrdg  8385  rdgsucmptf  8399  rdgsucmptnf  8400  frsucmpt  8409  frsucmptn  8410  ttrclselem1  9685  ttrclselem2  9686  rankidb  9760  rankval4  9827  dfac8clem  9992  cardaleph  10049  hsmexlem2  10387  axcc2  10397  uniimadomf  10505  nfseq  13983  seqof2  14032  rlim2  15469  nfsum1  15663  nfsum  15664  sumeq2ii  15666  fsumrelem  15780  o1fsum  15786  nfcprod1  15881  nfcprod  15882  fprodefsum  16068  prdsbas3  17451  prdsdsval2  17454  yonedalem4b  18244  gsum2d2lem  19910  coe1fzgsumdlem  22197  evl1gsumdlem  22250  ptcldmpt  23508  ptcnp  23516  cnmpt11  23557  cnmpt21  23565  cnmptk2  23580  prdsdsf  24262  prdsxmet  24264  ovolfiniun  25409  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  ovoliunnul  25415  volfiniun  25455  voliun  25462  mbfsup  25572  mbflim  25576  itg2splitlem  25656  itg2split  25657  itg2cnlem1  25669  isibl2  25674  nfitg1  25682  nfitg  25683  cbvitg  25684  itgabs  25743  dvlipcn  25906  lhop2  25927  dvfsumabs  25936  dvfsumrlim  25945  itgparts  25961  itgsubstlem  25962  ulmss  26313  itgulm2  26325  lgamgulmlem2  26947  lgamgulmlem6  26951  lgamgulm2  26953  lgseisenlem2  27294  dchrisumlem3  27409  sltval2  27575  nfseqs  28188  cnlnadjlem5  32007  dfimafnf  32567  2ndresdju  32580  esumfzf  34066  voliune  34226  volfiniune  34227  bnj1534  34850  bnj1542  34854  bnj958  34937  bnj1000  34938  bnj1446  35042  bnj1447  35043  bnj1448  35044  bnj1466  35050  bnj1467  35051  bnj1519  35062  bnj1520  35063  bnj1529  35067  onvf1odlem2  35098  cvmcov  35257  rdgssun  37373  exrecfnlem  37374  finxpreclem2  37385  finxpreclem6  37391  poimirlem23  37644  poimirlem27  37648  itgabsnc  37690  riotaocN  39209  cdleme32d  40445  cdleme32f  40447  ltrniotaval  40582  cdlemksv2  40848  cdlemkuv2  40868  cdlemk36  40914  cdlemk38  40916  cdlemk19x  40944  cdlemk11t  40947  evl1gprodd  42112  mzpsubst  42743  aomclem8  43057  mnringmulrcld  44224  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  nfrelp  44946  permaxrep  45003  permaxsep  45004  evth2f  45016  fvelrnbf  45019  evthf  45028  rfcnpre3  45034  rfcnpre4  45035  rfcnnnub  45037  refsum2cnlem1  45038  allbutfiinf  45423  monoordxr  45485  monoord2xr  45487  caucvgbf  45492  cvgcaule  45494  fmul01  45585  fmuldfeqlem1  45587  fmuldfeq  45588  fmul01lt1lem1  45589  fmul01lt1lem2  45590  fmul01lt1  45591  cncfmptss  45592  mulc1cncfg  45594  expcnfg  45596  fprodabs2  45600  climmulf  45609  climexp  45610  climsuse  45613  climrecf  45614  climinff  45616  climaddf  45620  mullimc  45621  idlimc  45631  limcperiod  45633  neglimc  45652  addlimc  45653  0ellimcdiv  45654  fnlimfv  45668  climreclf  45669  fnlimcnv  45672  fnlimfvre  45679  fnlimfvre2  45682  fnlimf  45683  fnlimabslt  45684  climfveqf  45685  climmptf  45686  climeldmeqf  45688  limsupref  45690  limsupbnd1f  45691  climbddf  45692  climeqf  45693  limsuppnfd  45707  climinf2  45712  limsuppnf  45716  limsupubuz  45718  climinfmpt  45720  limsupmnf  45726  limsupequz  45728  limsupre2  45730  limsupmnfuz  45732  limsupre3  45738  limsupre3uz  45741  limsupreuz  45742  climuz  45749  lmbr3  45752  limsupgt  45783  liminfvalxr  45788  liminfreuz  45808  liminflt  45810  xlimpnfxnegmnf  45819  liminfpnfuz  45821  xlimmnf  45846  xlimpnf  45847  dfxlim2  45853  xlimpnfxnegmnf2  45863  cncfshift  45879  icccncfext  45892  cncficcgt0  45893  cncfiooicclem1  45898  dvnmul  45948  dvnprodlem1  45951  itgsubsticclem  45980  stoweidlem3  46008  stoweidlem23  46028  stoweidlem26  46031  stoweidlem28  46033  stoweidlem29  46034  stoweidlem31  46036  stoweidlem34  46039  stoweidlem36  46041  stoweidlem42  46047  stoweidlem48  46053  stoweidlem51  46056  stoweidlem52  46057  stoweidlem59  46064  wallispilem5  46074  stirlinglem4  46082  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  fourierdlem20  46132  fourierdlem31  46143  fourierdlem79  46190  fourierdlem89  46200  fourierdlem91  46202  fourierdlem112  46223  fourierdlem115  46226  fourierd  46227  fourierclimd  46228  etransclem2  46241  etransclem48  46287  sge0revalmpt  46383  sge0fsummpt  46395  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0xadd  46440  sge0fsummptf  46441  sge0gtfsumgt  46448  iundjiun  46465  meadjiun  46471  voliunsge0lem  46477  meaiunincf  46488  meaiuninc3  46490  omeiunle  46522  omeiunltfirp  46524  ovncvrrp  46569  vonioo  46687  vonicc  46690  vonn0ioo2  46695  vonn0icc2  46697  pimltmnf2f  46702  pimgtpnf2f  46710  pimltpnf2f  46717  pimgtmnf2  46719  pimdecfgtioc  46720  issmff  46739  smfpimltxrmptf  46763  smfpreimagtf  46773  smflim  46782  smfpimgtxr  46785  smfpimgtxrmptf  46789  smfmullem4  46799  smflim2  46811  smfpimcclem  46812  smfpimcc  46813  smfsup  46819  smfsupmpt  46820  smfsupxr  46821  smfinflem  46822  smfinf  46823  smflimsuplem2  46826  smflimsuplem5  46829  smflimsuplem7  46831  smflimsup  46833  smfliminf  46836  fsupdm  46847  smfsupdmmbllem  46849  finfdm  46851  smfinfdmmbllem  46853  nfafv  47141  nfsetrecs  49679  setrec2fun  49685