Theorem fvexi 6770

Description: The value of a class exists. Inference form of fvex 6769. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
fvexi.1	⊢ 𝐴 = (𝐹‘𝐵)

Assertion

Ref	Expression
fvexi	⊢ 𝐴 ∈ V

Proof of Theorem fvexi

Step	Hyp	Ref	Expression
1		fvexi.1	. 2 ⊢ 𝐴 = (𝐹‘𝐵)
2		fvex 6769	. 2 ⊢ (𝐹‘𝐵) ∈ V
3	1, 2	eqeltri 2835	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837  df-iota 6376  df-fv 6426

This theorem is referenced by:  mptfvmpt  7086  ovex  7288  mapfienlem1  9094  climle  15277  climsup  15309  iserabs  15455  isumshft  15479  explecnv  15505  prodfclim1  15533  ressbas  16873  ressbasOLD  16874  ressbas2  16875  ressid  16880  ressval3d  16882  ressval3dOLD  16883  topnid  17063  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdsip  17089  prdsle  17090  prdsds  17092  prdshom  17095  prdsco  17096  pwselbasb  17116  pwsvscafval  17122  pwssca  17124  pwssnf1o  17126  imassca  17147  imasvsca  17148  imasle  17151  xpsrnbas  17199  xpssca  17204  xpsvsca  17205  isacs2  17279  homffval  17316  comfffval  17324  oppchomfval  17340  oppchomfvalOLD  17341  oppccofval  17343  oppccatid  17347  monfval  17361  oppcmon  17367  sectffval  17379  invffval  17387  rescbas  17458  rescbasOLD  17459  reschom  17460  rescco  17462  resccoOLD  17463  fullsubc  17481  isfunc  17495  isfuncd  17496  idfu2nd  17508  idfu1st  17510  cofu1st  17514  cofu2nd  17516  fucco  17596  fucid  17605  invfuc  17608  initoval  17624  termoval  17625  homafval  17660  arwval  17674  coafval  17695  coapm  17702  setccatid  17715  catchomfval  17733  catccofval  17735  catccatid  17737  elestrchom  17760  estrccatid  17764  xpcbas  17811  xpchomfval  17812  xpccofval  17815  1stf1  17825  1stf2  17826  2ndf1  17828  2ndf2  17829  prf1  17833  prf2fval  17834  evlf2  17852  evlf1  17854  curf1fval  17858  curf11  17860  curf12  17861  curf1cl  17862  curf2  17863  curf2cl  17865  hof2fval  17889  yonedalem4a  17909  yonedalem4c  17911  yonedalem3  17914  yonedainv  17915  isdrs  17934  ispos  17947  odupos  17961  pltfval  17964  lubfval  17983  lubeldm  17986  lubval  17989  glbfval  17996  glbeldm  17999  glbval  18002  odulub  18040  odujoin  18041  oduglb  18042  odumeet  18043  clatlem  18135  clatlubcl2  18137  clatglbcl2  18139  isdlat  18155  ipolt  18168  ipopos  18169  isacs4lem  18177  plusffval  18247  issstrmgm  18252  gsumvalx  18275  gsumval  18276  issubmnd  18327  ress0g  18328  ismhm  18347  0subm  18371  0mhm  18373  submacs  18380  pwsdiagmhm  18384  gsumz  18389  frmdplusg  18408  efmndplusg  18434  efmndmgm  18439  smndex1mgm  18461  grpinvfval  18533  grpsubfval  18538  grpsubfvalALT  18539  mulgfval  18617  mulgfvalALT  18618  mulgval  18619  issubg  18670  0subg  18695  subgacs  18704  nsgacs  18705  nmznsg  18711  eqgfval  18719  isghm  18749  gicen  18808  isga  18812  subgga  18821  orbstafun  18832  orbstaval  18833  orbsta  18834  cntzfval  18841  cntzval  18842  oppgplusfval  18867  symg2bas  18915  symgvalstruct  18919  symgvalstructOLD  18920  cayleylem2  18936  psgnfval  19023  odfval  19055  odinf  19085  dfod2  19086  pgpfi1  19115  pgp0  19116  sylow1lem2  19119  sylow3lem6  19152  lsmfval  19158  lsmvalx  19159  oppglsm  19162  pj1fval  19215  efglem  19237  efgrelexlemb  19271  efgcpbllemb  19276  frgpeccl  19282  frgpmhm  19286  vrgpval  19288  frgpuplem  19293  frgpupf  19294  frgpupval  19295  frgpup1  19296  frgpup3lem  19298  frgpnabllem2  19390  iscygodd  19403  prmcyg  19410  lt6abl  19411  gsumval3a  19419  gsumval3  19423  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumreidx  19433  gsumzaddlem  19437  gsumzadd  19438  gsumzsplit  19443  gsummptshft  19452  gsumzmhm  19453  gsumzoppg  19460  gsumzinv  19461  gsummptfidminv  19463  gsumsub  19464  gsumpt  19478  gsummptf1o  19479  gsum2dlem1  19486  gsum2dlem2  19487  gsum2d  19488  gsum2d2lem  19489  gsumxp2  19496  fsfnn0gsumfsffz  19499  nn0gsumfz  19500  gsummptnn0fz  19502  dprdfid  19535  dprdfinv  19537  dprdfadd  19538  dprdfeq0  19540  dmdprdsplitlem  19555  dpjidcl  19576  ablfacrplem  19583  ablfacrp  19584  ablfacrp2  19585  ablfac1a  19587  ablfac1b  19588  ablfac1c  19589  ablfac1eu  19591  pgpfaclem2  19600  ablfaclem2  19604  ablfaclem3  19605  2nsgsimpgd  19620  prmgrpsimpgd  19632  ablsimpgprmd  19633  mgpplusg  19639  mgpress  19650  mgpressOLD  19651  issrg  19658  ring1ne0  19745  gsumdixp  19763  pwsmgp  19772  opprmulfval  19779  dvdsrval  19802  isunit  19814  unitgrp  19824  unitlinv  19834  unitrinv  19835  dvrfval  19841  isdrng2  19916  drngmcl  19919  drngid2  19922  issubrg  19939  subrgugrp  19958  subrgacs  19983  sdrgacs  19984  cntzsdrg  19985  subdrgint  19986  isabv  19994  staffval  20022  islmod  20042  scaffval  20056  lcomfsupp  20078  mptscmfsupp0  20103  rmodislmod  20106  rmodislmodOLD  20107  lssset  20110  islss  20111  lsssn0  20124  lssacs  20144  lspfval  20150  lspval  20152  lspcl  20153  lspuni0  20187  lss0v  20193  0lmhm  20217  lmhmvsca  20222  islbs  20253  islbs3  20332  lbsextlem1  20335  lbsextlem3  20337  lbsextlem4  20338  lbsext  20340  rsp1  20408  2idlval  20417  qusrhm  20421  isnzr2  20447  isnzr2hash  20448  0ring  20454  01eq0ring  20456  0ring01eqbi  20457  rrgval  20471  rrgsupp  20475  expghm  20609  zrhrhmb  20624  zlmvsca  20639  zntoslem  20676  znfi  20679  znunithash  20684  psgnghm  20697  psgnghm2  20698  psgnevpmb  20704  ipffval  20765  ocvfval  20783  ocvval  20784  elocv  20785  thlbas  20813  thlle  20814  thlleval  20815  thloc  20816  pjfval  20823  pjdm  20824  pjpm  20825  isobs  20837  frlmbas  20872  frlmbasf  20877  frlmvscafval  20883  frlmvscavalb  20887  frlmsslss2  20892  frlmip  20895  uvcvval  20903  uvcvvcl  20904  frlmssuvc2  20912  frlmsslsp  20913  ellspd  20919  elfilspd  20920  islinds2  20930  islindf4  20955  aspval  20987  psrbas  21057  psrelbas  21058  psrplusg  21060  psrmulr  21063  psrvscafval  21069  psrvscacl  21072  psr0lid  21074  psrlidm  21082  psrridm  21083  resspsradd  21095  resspsrmul  21096  resspsrvsca  21097  mvrval2  21101  mplsubglem  21115  mpllsslem  21116  mplsubrglem  21120  mpladd  21123  mplmul  21125  ressmpladd  21140  ressmplmul  21141  ressmplvsca  21142  mplmon  21146  mplmonmul  21147  mplcoe1  21148  opsrle  21158  opsrtoslem2  21173  mplmon2  21179  evlslem4  21194  psrbagev1  21195  psrbagev1OLD  21196  evlslem2  21199  evlslem3  21200  evlsval2  21207  selvval  21238  mhpval  21240  ismhp3  21243  coe1sfi  21294  coe1fsupp  21295  mptcoe1fsupp  21296  coe1ae0  21297  ressply1add  21311  ressply1mul  21312  ressply1vsca  21313  gsumply1subr  21315  psropprmul  21319  coe1tmmul2fv  21359  coe1pwmulfv  21361  ply1coe  21377  cply1coe0  21380  cply1coe0bi  21381  gsummoncoe1  21385  evls1fval  21395  evls1val  21396  evls1rhmlem  21397  evls1sca  21399  evls1gsumadd  21400  evls1gsummul  21401  evl1val  21405  evl1fval1lem  21406  fveval1fvcl  21409  evl1sca  21410  evl1var  21412  evl1addd  21417  evl1subd  21418  evl1muld  21419  evl1expd  21421  pf1f  21426  pf1mpf  21428  pf1ind  21431  evl1gsummul  21436  mamures  21449  mndvcl  21450  mamucl  21458  mamuvs1  21462  mamuvs2  21463  matbas2d  21480  matecl  21482  mamumat1cl  21496  mat1comp  21497  mamulid  21498  mamurid  21499  mat1ov  21505  matsc  21507  mat1dimelbas  21528  mat1dimmul  21533  mat1f1o  21535  dmatval  21549  dmatmulcl  21557  scmatval  21561  scmatscmiddistr  21565  mavmulcl  21604  1mavmul  21605  marrepfval  21617  marrepeval  21620  marepvfval  21622  submafval  21636  mdetfval  21643  mdetunilem9  21677  mdetuni0  21678  m2detleiblem3  21686  m2detleiblem4  21687  minmar1fval  21703  minmar1eval  21706  symgmatr01  21711  gsummatr01lem3  21714  gsummatr01  21716  smadiadetlem1a  21720  smadiadetlem3  21725  invrvald  21733  cpmat  21766  mat2pmatfval  21780  mat2pmatbas  21783  decpmatfsupp  21826  decpmatmulsumfsupp  21830  pmatcollpw3lem  21840  pmatcollpw3fi1lem2  21844  pm2mpval  21852  mply1topmatcl  21862  chmatval  21886  chpmatfval  21887  chfacffsupp  21913  chfacfscmul0  21915  chfacfscmulfsupp  21916  chfacfpmmul0  21919  chfacfpmmulfsupp  21920  cpmidpmatlem2  21928  cpmadumatpolylem1  21938  imastopn  22779  uzrest  22956  tmdgsum2  23155  distgp  23158  indistgp  23159  snclseqg  23175  tsmsval  23190  tsms0  23201  tsmsres  23203  tsmsxplem1  23212  tsmsxplem2  23213  ussid  23320  isusp  23321  ressust  23323  cnextucn  23363  prdsxmetlem  23429  nrmmetd  23636  nmfval  23650  tngds  23717  tngdsOLD  23718  tngnm  23721  tngngp2  23722  tngngpd  23723  tngngp  23724  tngngp3  23726  nmo0  23805  xrrest  23876  climcncf  23969  cphsubrglem  24246  cphcjcl  24252  tcphex  24286  ipcau2  24303  cmsss  24420  rrxip  24459  minveclem4a  24499  minveclem4  24501  mbflimsup  24735  mbflim  24737  mdegfval  25132  mdegleb  25134  mdegldg  25136  deg1val  25166  uc1pval  25209  mon1pval  25211  q1pval  25223  r1pval  25226  ply1remlem  25232  ply1rem  25233  fta1glem1  25235  fta1glem2  25236  fta1blem  25238  ig1pval  25242  elqaalem3  25386  ulmcau  25459  ulmdvlem1  25464  ulmdvlem3  25466  mbfulm  25470  itgulm  25472  dchrplusg  26300  dchrmulid2  26305  dchrinvcl  26306  dchrptlem2  26318  dchrptlem3  26319  dchrsum2  26321  sumdchr2  26323  dchr2sum  26326  axtgcont1  26733  tgjustc1  26740  tgjustc2  26741  tglowdim1  26765  tgldimor  26767  tgldim0eq  26768  iscgrgd  26778  isismt  26799  tglnfn  26812  tglnunirn  26813  tglngval  26816  legval  26849  ishlg  26867  hlcgrex  26881  hlcgreulem  26882  mirval  26920  midexlem  26957  israg  26962  perpln1  26975  perpln2  26976  isperp  26977  ishpg  27024  midf  27041  ismidb  27043  lmif  27050  islmib  27052  iscgra  27074  isinag  27103  isleag  27112  iseqlg  27132  ttgval  27140  ttgitvval  27152  setsvtx  27308  uhgrunop  27348  incistruhgr  27352  upgrunop  27392  umgrunop  27394  usgriedgleord  27498  uspgredgleord  27502  uhgr0vsize0  27509  lfuhgr1v0e  27524  uhgrspanop  27566  upgrspanop  27567  umgrspanop  27568  usgrspanop  27569  uhgrspan1lem1  27570  upgrres1lem1  27579  usgredgffibi  27594  fusgredgfi  27595  usgr1v0e  27596  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  nbfusgrlevtxm1  27647  nbfusgrlevtxm2  27648  uvtx01vtx  27667  cplgr1vlem  27699  cplgr1v  27700  cusgrsize2inds  27723  cusgrfilem3  27727  sizusglecusg  27733  fusgrmaxsize  27734  vtxdgfval  27737  vtxdun  27751  vtxd0nedgb  27758  p1evtxdeqlem  27782  p1evtxdeq  27783  p1evtxdp1  27784  usgrvd0nedg  27803  vtxdginducedm1lem1  27809  vtxdginducedm1lem4  27812  vtxdginducedm1  27813  vtxdginducedm1fi  27814  finsumvtxdg2ssteplem4  27818  rusgrnumwrdl2  27856  wksfval  27879  iswlkg  27883  wlkonprop  27928  wlkp1lem3  27945  wlkp1lem8  27950  wlkp1  27951  wksonproplem  27974  wwlks  28101  wwlksnon  28117  wspthsnon  28118  clwwlk  28248  0wlkonlem2  28384  conngrv2edg  28460  eupthp1  28481  eupth2eucrct  28482  eupthvdres  28500  eupth2lem3  28501  eupth2lemb  28502  3cyclfrgrrn  28551  frgrwopreglem1  28577  frgrwopreg1  28583  imsmetlem  28953  dipfval  28965  sspval  28986  islno  29016  nmooval  29026  nmounbseqi  29040  nmobndseqi  29042  0ofval  29050  0oval  29051  ajfval  29072  isph  29085  phpar  29087  ajval  29124  ubthlem1  29133  ubthlem2  29134  minvecolem4b  29141  minvecolem4  29143  minvecolem5  29144  hlex  29161  ressplusf  31137  ressnm  31138  oppglt  31142  ressprs  31143  oduprs  31144  ismnt  31163  mgcval  31167  gsummptres  31214  gsummptres2  31215  gsumpart  31217  gsumhashmul  31218  inftmrel  31336  isinftm  31337  gsumvsca1  31381  ress1r  31388  rdivmuldivd  31390  ringinvval  31391  dvrcan5  31392  rmfsupp2  31394  ofldlt1  31414  resvsca  31431  quslmod  31456  islinds5  31465  ellspds  31466  elrsp  31471  linds2eq  31477  elringlsm  31483  lsmsnpridl  31488  grplsm0l  31493  qusima  31496  nsgmgc  31499  nsgqusf1o  31503  elrspunidl  31508  prmidl0  31528  idlsrgbas  31551  idlsrgplusg  31552  idlsrgmulr  31554  idlsrgtset  31555  rprmval  31566  fply1  31569  dimval  31588  dimvalfi  31589  lvecdim0  31592  mdetpmtr1  31675  rspectopn  31719  zarcls0  31720  zarcls  31726  zartopn  31727  zarmxt1  31732  rhmpreimacnlem  31736  rhmpreimacn  31737  pstmfval  31748  ordtrest2NEW  31775  ordtconnlem1  31776  fsumcvg4  31802  pl1cn  31807  qqhval  31824  sibf0  32201  sitgclg  32209  sitgaddlemb  32215  eulerpartlemgvv  32243  afsval  32551  pthhashvtx  32989  usgrcyclgt2v  32993  cusgr3cyclex  32998  acycgr2v  33012  cusgracyclt3v  33018  mrsubfval  33370  mrsubcv  33372  mrsubff  33374  mrsubrn  33375  elmrsubrn  33382  msubfval  33386  msubff  33392  mpstval  33397  elmpst  33398  msrval  33400  mstaval  33406  msubvrs  33422  mclsssvlem  33424  mclsval  33425  mclsind  33432  mppsval  33434  climlec3  33605  sdclem2  35827  sdclem1  35828  caures  35845  heiborlem3  35898  heibor  35906  grpokerinj  35978  rngoi  35984  dvrunz  36039  isdrngo1  36041  isdrngo2  36043  isrngohom  36050  idlval  36098  isidl  36099  0idl  36110  0rngo  36112  divrngidl  36113  smprngopr  36137  igenval  36146  lshpset  36919  lsatset  36931  lcvfbr  36961  islfl  37001  lfl0f  37010  lfl1  37011  lfladd0l  37015  lflnegl  37017  lflvscl  37018  lflvsdi1  37019  lflvsdi2  37020  lflvsdi2a  37021  lflvsass  37022  lfl0sc  37023  lflsc0N  37024  lfl1sc  37025  lkr0f  37035  lkrsc  37038  eqlkr2  37041  ldualvbase  37067  ldualfvadd  37069  ldualvaddval  37072  ldualsca  37073  ldualfvs  37077  ldualvsval  37079  isopos  37121  cmtfvalN  37151  cvrfval  37209  pats  37226  glbconN  37318  llnset  37446  lplnset  37470  lvolset  37513  lineset  37679  isline  37680  pointsetN  37682  psubspset  37685  ispsubsp  37686  pmapval  37698  paddfval  37738  paddval  37739  pclfvalN  37830  pclvalN  37831  polfvalN  37845  polvalN  37846  psubclsetN  37877  ispsubclN  37878  watvalN  37934  lhpset  37936  lautset  38023  islaut  38024  pautsetN  38039  ispautN  38040  ldilset  38050  ltrnset  38059  dilsetN  38094  cdleme26e  38300  cdleme26eALTN  38302  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32a  38382  cdleme40m  38408  cdleme40n  38409  cdleme42b  38419  tgrpbase  38687  tgrpopr  38688  istendo  38701  tendopl  38717  tendo02  38728  erngbase  38742  erngfplus  38743  erngfmul  38746  erngbase-rN  38750  erngfplus-rN  38751  erngfmul-rN  38754  cdlemk36  38854  cdlemkid  38877  dvasca  38947  dvavbase  38954  dvafvadd  38955  dvafvsca  38957  diafval  38972  diaval  38973  dvhsca  39023  dvhvbase  39028  dvhfvadd  39032  dvhfvsca  39041  docafvalN  39063  docavalN  39064  djafvalN  39075  djavalN  39076  dibfval  39082  dibopelvalN  39084  dibopelval2  39086  dibelval3  39088  diblsmopel  39112  dicfval  39116  dicval  39117  cdlemn11a  39148  dihvalcqpre  39176  dihopelvalcpre  39189  dihord6apre  39197  dihpN  39277  dochfval  39291  dochval  39292  djhfval  39338  djhval  39339  islpolN  39424  lpolconN  39428  dochpolN  39431  lcfrlem9  39491  lcd0vvalN  39554  mapdval  39569  mapd1o  39589  mapdunirnN  39591  mapdhval  39665  mapdhval0  39666  hvmapfval  39700  hvmapval  39701  hdmap1fval  39737  hdmap1vallem  39738  hgmapfval  39827  hlhilset  39875  hlhilbase  39877  hlhilplus  39878  hlhilvsca  39892  hlhilip  39893  hlhilnvl  39895  hlhillsm  39901  hlhillcs  39903  frlmfielbas  40157  frlm0vald  40187  evlsval3  40195  evlsbagval  40198  fsuppind  40202  fsuppssind  40205  mhpind  40206  mhphf  40208  islssfgi  40813  pwssplit4  40830  frlmpwfi  40839  mendplusgfval  40926  mendmulrfval  40928  mendvscafval  40931  idomrootle  40936  idomodle  40937  deg1mhm  40948  mnringelbased  41721  mnring0g2d  41727  mnringmulrd  41728  mnringmulrcld  41735  dvgrat  41819  uzmptshftfval  41853  climexp  43036  climinf  43037  climneg  43041  climdivf  43043  climconstmpt  43089  climresmpt  43090  climsubmpt  43091  fnlimfvre  43105  limsupvaluz  43139  limsupequzmpt2  43149  climuzlem  43174  climisp  43177  climxrrelem  43180  climxrre  43181  limsupgtlem  43208  liminflelimsupuz  43216  liminfgelimsupuz  43219  liminfequzmpt2  43222  liminfvaluz  43223  limsupvaluz3  43229  climliminflimsupd  43232  liminfreuzlem  43233  liminfltlem  43235  liminflimsupclim  43238  liminflbuz2  43246  liminfpnfuz  43247  xlimclim2lem  43270  climxlim2  43277  sge0isum  43855  sge0uzfsumgt  43872  sge0seq  43874  meaiunlelem  43896  caragendifcl  43942  omeiunle  43945  omeiunltfirp  43947  carageniuncl  43951  caragensal  43953  opnssborel  44063  smflimlem6  44198  smfpimcc  44228  smflimmpt  44230  smflimsuplem4  44243  smflimsuplem6  44245  smflimsuplem8  44247  smfliminflem  44250  isomuspgrlem2  45173  ushrisomgr  45181  upwlksfval  45185  isupwlkg  45187  ismgmhm  45225  issubmgm2  45232  submgmacs  45246  copisnmnd  45251  0ringdif  45316  rnghmval  45337  isrnghm  45338  c0snmgmhm  45360  c0snmhm  45361  zrrnghm  45363  zlidlring  45374  cznrng  45401  cznnring  45402  rngchomfvalALTV  45430  rngccofvalALTV  45433  rngccatidALTV  45435  ringchomfvalALTV  45493  ringccofvalALTV  45496  ringccatidALTV  45498  rngcrescrhm  45531  rngcrescrhmALTV  45549  ofaddmndmap  45567  suppmptcfin  45603  mptcfsupp  45604  dmatALTbas  45630  lcoop  45640  linccl  45643  lcosn0  45649  lincvalsc0  45650  lcoc0  45651  linc0scn0  45652  linc1  45654  lincscmcl  45661  islinindfis  45678  lincext1  45683  lincext2  45684  lindslinindimp2lem2  45688  lindslinindimp2lem3  45689  lindsrng01  45697  snlindsntorlem  45699  snlindsntor  45700  ldepspr  45702  lincresunit1  45706  lincresunit2  45707  lines  45965  line  45966  rrxlines  45967  sphere  45981  rrxsphere  45982  functhinclem1  46210  thincciso  46218