Theorem fvexi 6825

Description: The value of a class exists. Inference form of fvex 6824. (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 6824	. 2 ⊢ (𝐹‘𝐵) ∈ V
3	1, 2	eqeltri 2834	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1540   ∈ wcel 2105  Vcvv 3441  ‘cfv 6465

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-nul 5245

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-sn 4572  df-pr 4574  df-uni 4851  df-iota 6417  df-fv 6473

This theorem is referenced by:  mptfvmpt  7143  ovex  7348  mapfienlem1  9234  climle  15421  climsup  15453  iserabs  15599  isumshft  15623  explecnv  15649  prodfclim1  15677  ressbas  17017  ressbasOLD  17018  ressbas2  17019  ressid  17024  ressval3d  17026  ressval3dOLD  17027  topnid  17216  prdsplusg  17239  prdsmulr  17240  prdsvsca  17241  prdsip  17242  prdsle  17243  prdsds  17245  prdshom  17248  prdsco  17249  pwselbasb  17269  pwsvscafval  17275  pwssca  17277  pwssnf1o  17279  imassca  17300  imasvsca  17301  imasle  17304  xpsrnbas  17352  xpssca  17357  xpsvsca  17358  isacs2  17432  homffval  17469  comfffval  17477  oppchomfval  17493  oppchomfvalOLD  17494  oppccofval  17496  oppccatid  17500  monfval  17514  oppcmon  17520  sectffval  17532  invffval  17540  rescbas  17611  rescbasOLD  17612  reschom  17613  rescco  17615  resccoOLD  17616  fullsubc  17635  isfunc  17649  isfuncd  17650  idfu2nd  17662  idfu1st  17664  cofu1st  17668  cofu2nd  17670  fucco  17750  fucid  17759  invfuc  17762  initoval  17778  termoval  17779  homafval  17814  arwval  17828  coafval  17849  coapm  17856  setccatid  17869  catchomfval  17887  catccofval  17889  catccatid  17891  elestrchom  17914  estrccatid  17918  xpcbas  17965  xpchomfval  17966  xpccofval  17969  1stf1  17979  1stf2  17980  2ndf1  17982  2ndf2  17983  prf1  17987  prf2fval  17988  evlf2  18006  evlf1  18008  curf1fval  18012  curf11  18014  curf12  18015  curf1cl  18016  curf2  18017  curf2cl  18019  hof2fval  18043  yonedalem4a  18063  yonedalem4c  18065  yonedalem3  18068  yonedainv  18069  isdrs  18089  ispos  18102  odupos  18116  pltfval  18119  lubfval  18138  lubeldm  18141  lubval  18144  glbfval  18151  glbeldm  18154  glbval  18157  odulub  18195  odujoin  18196  oduglb  18197  odumeet  18198  clatlem  18290  clatlubcl2  18292  clatglbcl2  18294  isdlat  18310  ipolt  18323  ipopos  18324  isacs4lem  18332  plusffval  18402  issstrmgm  18407  gsumvalx  18430  gsumval  18431  issubmnd  18482  ress0g  18483  ismhm  18502  0subm  18526  0mhm  18528  submacs  18535  pwsdiagmhm  18539  gsumz  18544  frmdplusg  18562  efmndplusg  18588  efmndmgm  18593  smndex1mgm  18615  grpinvfval  18687  grpsubfval  18692  grpsubfvalALT  18693  mulgfval  18771  mulgfvalALT  18772  mulgval  18773  issubg  18824  0subg  18849  subgacs  18858  nsgacs  18859  nmznsg  18865  eqgfval  18873  isghm  18903  gicen  18962  isga  18966  subgga  18975  orbstafun  18986  orbstaval  18987  orbsta  18988  cntzfval  18995  cntzval  18996  oppgplusfval  19021  symg2bas  19069  symgvalstruct  19073  symgvalstructOLD  19074  cayleylem2  19090  psgnfval  19177  odfval  19209  odinf  19239  dfod2  19240  pgpfi1  19269  pgp0  19270  sylow1lem2  19273  sylow3lem6  19306  lsmfval  19312  lsmvalx  19313  oppglsm  19316  pj1fval  19368  efglem  19390  efgrelexlemb  19424  efgcpbllemb  19429  frgpeccl  19435  frgpmhm  19439  vrgpval  19441  frgpuplem  19446  frgpupf  19447  frgpupval  19448  frgpup1  19449  frgpup3lem  19451  frgpnabllem2  19543  iscygodd  19556  prmcyg  19563  lt6abl  19564  gsumval3a  19572  gsumval3  19576  gsumzres  19578  gsumzcl2  19579  gsumzf1o  19581  gsumreidx  19586  gsumzaddlem  19590  gsumzadd  19591  gsumzsplit  19596  gsummptshft  19605  gsumzmhm  19606  gsumzoppg  19613  gsumzinv  19614  gsummptfidminv  19616  gsumsub  19617  gsumpt  19631  gsummptf1o  19632  gsum2dlem1  19639  gsum2dlem2  19640  gsum2d  19641  gsum2d2lem  19642  gsumxp2  19649  fsfnn0gsumfsffz  19652  nn0gsumfz  19653  gsummptnn0fz  19655  dprdfid  19688  dprdfinv  19690  dprdfadd  19691  dprdfeq0  19693  dmdprdsplitlem  19708  dpjidcl  19729  ablfacrplem  19736  ablfacrp  19737  ablfacrp2  19738  ablfac1a  19740  ablfac1b  19741  ablfac1c  19742  ablfac1eu  19744  pgpfaclem2  19753  ablfaclem2  19757  ablfaclem3  19758  2nsgsimpgd  19773  prmgrpsimpgd  19785  ablsimpgprmd  19786  mgpplusg  19792  mgpress  19803  mgpressOLD  19804  issrg  19811  ring1ne0  19898  gsumdixp  19916  pwsmgp  19925  opprmulfval  19932  dvdsrval  19955  isunit  19967  unitgrp  19977  unitlinv  19987  unitrinv  19988  dvrfval  19994  isdrng2  20073  drngmcl  20076  drngid2  20079  issubrg  20096  subrgugrp  20115  subrgacs  20140  sdrgacs  20141  cntzsdrg  20142  subdrgint  20143  isabv  20151  staffval  20179  islmod  20199  scaffval  20213  lcomfsupp  20235  mptscmfsupp0  20260  rmodislmod  20263  rmodislmodOLD  20264  lssset  20267  islss  20268  lsssn0  20281  lssacs  20301  lspfval  20307  lspval  20309  lspcl  20310  lspuni0  20344  lss0v  20350  0lmhm  20374  lmhmvsca  20379  islbs  20410  islbs3  20489  lbsextlem1  20492  lbsextlem3  20494  lbsextlem4  20495  lbsext  20497  rsp1  20567  2idlval  20576  qusrhm  20580  isnzr2  20606  isnzr2hash  20607  0ring  20613  01eq0ring  20615  0ring01eqbi  20616  rrgval  20630  rrgsupp  20634  expghm  20769  zrhrhmb  20784  zlmvsca  20799  zntoslem  20836  znfi  20839  znunithash  20844  psgnghm  20857  psgnghm2  20858  psgnevpmb  20864  ipffval  20925  ocvfval  20943  ocvval  20944  elocv  20945  thlbas  20973  thlbasOLD  20974  thlle  20975  thlleOLD  20976  thlleval  20977  thloc  20978  pjfval  20985  pjdm  20986  pjpm  20987  isobs  20999  frlmbas  21034  frlmbasf  21039  frlmvscafval  21045  frlmvscavalb  21049  frlmsslss2  21054  frlmip  21057  uvcvval  21065  uvcvvcl  21066  frlmssuvc2  21074  frlmsslsp  21075  ellspd  21081  elfilspd  21082  islinds2  21092  islindf4  21117  aspval  21149  psrbas  21219  psrelbas  21220  psrplusg  21222  psrmulr  21225  psrvscafval  21231  psrvscacl  21234  psr0lid  21236  psrlidm  21244  psrridm  21245  resspsradd  21257  resspsrmul  21258  resspsrvsca  21259  mvrval2  21263  mplsubglem  21277  mpllsslem  21278  mplsubrglem  21282  mpladd  21285  mplmul  21287  ressmpladd  21302  ressmplmul  21303  ressmplvsca  21304  mplmon  21308  mplmonmul  21309  mplcoe1  21310  opsrle  21320  opsrtoslem2  21335  mplmon2  21341  evlslem4  21356  psrbagev1  21357  psrbagev1OLD  21358  evlslem2  21361  evlslem3  21362  evlsval2  21369  selvval  21400  mhpval  21402  ismhp3  21405  coe1sfi  21456  coe1fsupp  21457  mptcoe1fsupp  21458  coe1ae0  21459  ressply1add  21473  ressply1mul  21474  ressply1vsca  21475  gsumply1subr  21477  psropprmul  21481  coe1tmmul2fv  21521  coe1pwmulfv  21523  ply1coe  21539  cply1coe0  21542  cply1coe0bi  21543  gsummoncoe1  21547  evls1fval  21557  evls1val  21558  evls1rhmlem  21559  evls1sca  21561  evls1gsumadd  21562  evls1gsummul  21563  evl1val  21567  evl1fval1lem  21568  fveval1fvcl  21571  evl1sca  21572  evl1var  21574  evl1addd  21579  evl1subd  21580  evl1muld  21581  evl1expd  21583  pf1f  21588  pf1mpf  21590  pf1ind  21593  evl1gsummul  21598  mamures  21611  mndvcl  21612  mamucl  21620  mamuvs1  21624  mamuvs2  21625  matbas2d  21644  matecl  21646  mamumat1cl  21660  mat1comp  21661  mamulid  21662  mamurid  21663  mat1ov  21669  matsc  21671  mat1dimelbas  21692  mat1dimmul  21697  mat1f1o  21699  dmatval  21713  dmatmulcl  21721  scmatval  21725  scmatscmiddistr  21729  mavmulcl  21768  1mavmul  21769  marrepfval  21781  marrepeval  21784  marepvfval  21786  submafval  21800  mdetfval  21807  mdetunilem9  21841  mdetuni0  21842  m2detleiblem3  21850  m2detleiblem4  21851  minmar1fval  21867  minmar1eval  21870  symgmatr01  21875  gsummatr01lem3  21878  gsummatr01  21880  smadiadetlem1a  21884  smadiadetlem3  21889  invrvald  21897  cpmat  21930  mat2pmatfval  21944  mat2pmatbas  21947  decpmatfsupp  21990  decpmatmulsumfsupp  21994  pmatcollpw3lem  22004  pmatcollpw3fi1lem2  22008  pm2mpval  22016  mply1topmatcl  22026  chmatval  22050  chpmatfval  22051  chfacffsupp  22077  chfacfscmul0  22079  chfacfscmulfsupp  22080  chfacfpmmul0  22083  chfacfpmmulfsupp  22084  cpmidpmatlem2  22092  cpmadumatpolylem1  22102  imastopn  22943  uzrest  23120  tmdgsum2  23319  distgp  23322  indistgp  23323  snclseqg  23339  tsmsval  23354  tsms0  23365  tsmsres  23367  tsmsxplem1  23376  tsmsxplem2  23377  ussid  23484  isusp  23485  ressust  23487  cnextucn  23527  prdsxmetlem  23593  nrmmetd  23802  nmfval  23816  tngds  23883  tngdsOLD  23884  tngnm  23887  tngngp2  23888  tngngpd  23889  tngngp  23890  tngngp3  23892  nmo0  23971  xrrest  24042  climcncf  24135  cphsubrglem  24413  cphcjcl  24419  tcphex  24453  ipcau2  24470  cmsss  24587  rrxip  24626  minveclem4a  24666  minveclem4  24668  mbflimsup  24902  mbflim  24904  mdegfval  25299  mdegleb  25301  mdegldg  25303  deg1val  25333  uc1pval  25376  mon1pval  25378  q1pval  25390  r1pval  25393  ply1remlem  25399  ply1rem  25400  fta1glem1  25402  fta1glem2  25403  fta1blem  25405  ig1pval  25409  elqaalem3  25553  ulmcau  25626  ulmdvlem1  25631  ulmdvlem3  25633  mbfulm  25637  itgulm  25639  dchrplusg  26467  dchrmulid2  26472  dchrinvcl  26473  dchrptlem2  26485  dchrptlem3  26486  dchrsum2  26488  sumdchr2  26490  dchr2sum  26493  axtgcont1  26938  tgjustc1  26945  tgjustc2  26946  tglowdim1  26970  tgldimor  26972  tgldim0eq  26973  iscgrgd  26983  isismt  27004  tglnfn  27017  tglnunirn  27018  tglngval  27021  legval  27054  ishlg  27072  hlcgrex  27086  hlcgreulem  27087  mirval  27125  midexlem  27162  israg  27167  perpln1  27180  perpln2  27181  isperp  27182  ishpg  27229  midf  27246  ismidb  27248  lmif  27255  islmib  27257  iscgra  27279  isinag  27308  isleag  27317  iseqlg  27337  ttgval  27345  ttgvalOLD  27346  ttgitvval  27358  setsvtx  27514  uhgrunop  27554  incistruhgr  27558  upgrunop  27598  umgrunop  27600  usgriedgleord  27704  uspgredgleord  27708  uhgr0vsize0  27715  lfuhgr1v0e  27730  uhgrspanop  27772  upgrspanop  27773  umgrspanop  27774  usgrspanop  27775  uhgrspan1lem1  27776  upgrres1lem1  27785  usgredgffibi  27800  fusgredgfi  27801  usgr1v0e  27802  nbgr2vtx1edg  27826  nbuhgr2vtx1edgb  27828  nbfusgrlevtxm1  27853  nbfusgrlevtxm2  27854  uvtx01vtx  27873  cplgr1vlem  27905  cplgr1v  27906  cusgrsize2inds  27929  cusgrfilem3  27933  sizusglecusg  27939  fusgrmaxsize  27940  vtxdgfval  27943  vtxdun  27957  vtxd0nedgb  27964  p1evtxdeqlem  27988  p1evtxdeq  27989  p1evtxdp1  27990  usgrvd0nedg  28009  vtxdginducedm1lem1  28015  vtxdginducedm1lem4  28018  vtxdginducedm1  28019  vtxdginducedm1fi  28020  finsumvtxdg2ssteplem4  28024  rusgrnumwrdl2  28062  wksfval  28085  iswlkg  28089  wlkonprop  28135  wlkp1lem3  28152  wlkp1lem8  28157  wlkp1  28158  wksonproplem  28181  wksonproplemOLD  28182  wwlks  28309  wwlksnon  28325  wspthsnon  28326  clwwlk  28456  0wlkonlem2  28592  conngrv2edg  28668  eupthp1  28689  eupth2eucrct  28690  eupthvdres  28708  eupth2lem3  28709  eupth2lemb  28710  3cyclfrgrrn  28759  frgrwopreglem1  28785  frgrwopreg1  28791  imsmetlem  29161  dipfval  29173  sspval  29194  islno  29224  nmooval  29234  nmounbseqi  29248  nmobndseqi  29250  0ofval  29258  0oval  29259  ajfval  29280  isph  29293  phpar  29295  ajval  29332  ubthlem1  29341  ubthlem2  29342  minvecolem4b  29349  minvecolem4  29351  minvecolem5  29352  hlex  29369  ressplusf  31343  ressnm  31344  oppglt  31348  ressprs  31349  oduprs  31350  ismnt  31369  mgcval  31373  gsummptres  31420  gsummptres2  31421  gsumpart  31423  gsumhashmul  31424  inftmrel  31542  isinftm  31543  gsumvsca1  31587  ress1r  31594  rdivmuldivd  31596  ringinvval  31597  dvrcan5  31598  rmfsupp2  31600  ofldlt1  31620  resvsca  31633  quslmod  31658  islinds5  31668  ellspds  31669  elrsp  31674  linds2eq  31680  elringlsm  31686  lsmsnpridl  31691  grplsm0l  31696  qusima  31699  nsgmgc  31702  nsgqusf1o  31706  elrspunidl  31711  prmidl0  31731  idlsrgbas  31754  idlsrgplusg  31755  idlsrgmulr  31757  idlsrgtset  31758  rprmval  31769  fply1  31772  dimval  31792  dimvalfi  31793  lvecdim0  31796  mdetpmtr1  31879  rspectopn  31923  zarcls0  31924  zarcls  31930  zartopn  31931  zarmxt1  31936  rhmpreimacnlem  31940  rhmpreimacn  31941  pstmfval  31952  ordtrest2NEW  31979  ordtconnlem1  31980  fsumcvg4  32006  pl1cn  32011  qqhval  32030  sibf0  32407  sitgclg  32415  sitgaddlemb  32421  eulerpartlemgvv  32449  afsval  32757  pthhashvtx  33194  usgrcyclgt2v  33198  cusgr3cyclex  33203  acycgr2v  33217  cusgracyclt3v  33223  mrsubfval  33575  mrsubcv  33577  mrsubff  33579  mrsubrn  33580  elmrsubrn  33587  msubfval  33591  msubff  33597  mpstval  33602  elmpst  33603  msrval  33605  mstaval  33611  msubvrs  33627  mclsssvlem  33629  mclsval  33630  mclsind  33637  mppsval  33639  climlec3  33800  sdclem2  35956  sdclem1  35957  caures  35974  heiborlem3  36027  heibor  36035  grpokerinj  36107  rngoi  36113  dvrunz  36168  isdrngo1  36170  isdrngo2  36172  isrngohom  36179  idlval  36227  isidl  36228  0idl  36239  0rngo  36241  divrngidl  36242  smprngopr  36266  igenval  36275  lshpset  37196  lsatset  37208  lcvfbr  37238  islfl  37278  lfl0f  37287  lfl1  37288  lfladd0l  37292  lflnegl  37294  lflvscl  37295  lflvsdi1  37296  lflvsdi2  37297  lflvsdi2a  37298  lflvsass  37299  lfl0sc  37300  lflsc0N  37301  lfl1sc  37302  lkr0f  37312  lkrsc  37315  eqlkr2  37318  ldualvbase  37344  ldualfvadd  37346  ldualvaddval  37349  ldualsca  37350  ldualfvs  37354  ldualvsval  37356  isopos  37398  cmtfvalN  37428  cvrfval  37486  pats  37503  glbconNOLD  37596  llnset  37724  lplnset  37748  lvolset  37791  lineset  37957  isline  37958  pointsetN  37960  psubspset  37963  ispsubsp  37964  pmapval  37976  paddfval  38016  paddval  38017  pclfvalN  38108  pclvalN  38109  polfvalN  38123  polvalN  38124  psubclsetN  38155  ispsubclN  38156  watvalN  38212  lhpset  38214  lautset  38301  islaut  38302  pautsetN  38317  ispautN  38318  ldilset  38328  ltrnset  38337  dilsetN  38372  cdleme26e  38578  cdleme26eALTN  38580  cdleme26fALTN  38581  cdleme26f  38582  cdleme26f2ALTN  38583  cdleme26f2  38584  cdlemefs32sn1aw  38633  cdleme43fsv1snlem  38639  cdleme41sn3a  38652  cdleme32a  38660  cdleme40m  38686  cdleme40n  38687  cdleme42b  38697  tgrpbase  38965  tgrpopr  38966  istendo  38979  tendopl  38995  tendo02  39006  erngbase  39020  erngfplus  39021  erngfmul  39024  erngbase-rN  39028  erngfplus-rN  39029  erngfmul-rN  39032  cdlemk36  39132  cdlemkid  39155  dvasca  39225  dvavbase  39232  dvafvadd  39233  dvafvsca  39235  diafval  39250  diaval  39251  dvhsca  39301  dvhvbase  39306  dvhfvadd  39310  dvhfvsca  39319  docafvalN  39341  docavalN  39342  djafvalN  39353  djavalN  39354  dibfval  39360  dibopelvalN  39362  dibopelval2  39364  dibelval3  39366  diblsmopel  39390  dicfval  39394  dicval  39395  cdlemn11a  39426  dihvalcqpre  39454  dihopelvalcpre  39467  dihord6apre  39475  dihpN  39555  dochfval  39569  dochval  39570  djhfval  39616  djhval  39617  islpolN  39702  lpolconN  39706  dochpolN  39709  lcfrlem9  39769  lcd0vvalN  39832  mapdval  39847  mapd1o  39867  mapdunirnN  39869  mapdhval  39943  mapdhval0  39944  hvmapfval  39978  hvmapval  39979  hdmap1fval  40015  hdmap1vallem  40016  hgmapfval  40105  hlhilset  40153  hlhilbase  40155  hlhilplus  40156  hlhilvsca  40170  hlhilip  40171  hlhilnvl  40173  hlhillsm  40179  hlhillcs  40181  frlmfielbas  40434  frlm0vald  40465  evlsval3  40475  evlsbagval  40478  fsuppind  40482  fsuppssind  40485  mhpind  40486  mhphf  40488  islssfgi  41101  pwssplit4  41118  frlmpwfi  41127  mendplusgfval  41214  mendmulrfval  41216  mendvscafval  41219  idomrootle  41224  idomodle  41225  deg1mhm  41236  mnringelbased  42053  mnring0g2d  42059  mnringmulrd  42060  mnringmulrcld  42067  dvgrat  42151  uzmptshftfval  42185  climexp  43383  climinf  43384  climneg  43388  climdivf  43390  climconstmpt  43436  climresmpt  43437  climsubmpt  43438  fnlimfvre  43452  limsupvaluz  43486  limsupequzmpt2  43496  climuzlem  43521  climisp  43524  climxrrelem  43527  climxrre  43528  limsupgtlem  43555  liminflelimsupuz  43563  liminfgelimsupuz  43566  liminfequzmpt2  43569  liminfvaluz  43570  limsupvaluz3  43576  climliminflimsupd  43579  liminfreuzlem  43580  liminfltlem  43582  liminflimsupclim  43585  liminflbuz2  43593  liminfpnfuz  43594  xlimclim2lem  43617  climxlim2  43624  sge0isum  44203  sge0uzfsumgt  44220  sge0seq  44222  meaiunlelem  44244  caragendifcl  44290  omeiunle  44293  omeiunltfirp  44295  carageniuncl  44299  caragensal  44301  opnssborel  44411  smflimlem6  44552  smfpimcc  44584  smflimmpt  44586  smflimsuplem4  44599  smflimsuplem6  44601  smflimsuplem8  44603  smfliminflem  44606  isomuspgrlem2  45537  ushrisomgr  45545  upwlksfval  45549  isupwlkg  45551  ismgmhm  45589  issubmgm2  45596  submgmacs  45610  copisnmnd  45615  0ringdif  45680  rnghmval  45701  isrnghm  45702  c0snmgmhm  45724  c0snmhm  45725  zrrnghm  45727  zlidlring  45738  cznrng  45765  cznnring  45766  rngchomfvalALTV  45794  rngccofvalALTV  45797  rngccatidALTV  45799  ringchomfvalALTV  45857  ringccofvalALTV  45860  ringccatidALTV  45862  rngcrescrhm  45895  rngcrescrhmALTV  45913  ofaddmndmap  45931  suppmptcfin  45967  mptcfsupp  45968  dmatALTbas  45994  lcoop  46004  linccl  46007  lcosn0  46013  lincvalsc0  46014  lcoc0  46015  linc0scn0  46016  linc1  46018  lincscmcl  46025  islinindfis  46042  lincext1  46047  lincext2  46048  lindslinindimp2lem2  46052  lindslinindimp2lem3  46053  lindsrng01  46061  snlindsntorlem  46063  snlindsntor  46064  ldepspr  46066  lincresunit1  46070  lincresunit2  46071  lines  46329  line  46330  rrxlines  46331  sphere  46345  rrxsphere  46346  functhinclem1  46574  thincciso  46582