Theorem fvexi 6416

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

Syntax hints:   = wceq 1637   ∈ wcel 2155  Vcvv 3387  ‘cfv 6095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-nul 4977

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-rex 3098  df-v 3389  df-sbc 3628  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-sn 4365  df-pr 4367  df-uni 4624  df-iota 6058  df-fv 6103

This theorem is referenced by:  mptfvmpt  6709  ovex  6900  mapfienlem1  8543  climle  14587  climsup  14617  iserabs  14763  isumshft  14787  explecnv  14813  prodfclim1  14840  ressbas  16135  ressbas2  16136  ressid  16140  ressval3d  16142  topnid  16295  prdsplusg  16317  prdsmulr  16318  prdsvsca  16319  prdsip  16320  prdsle  16321  prdsds  16323  prdshom  16326  prdsco  16327  pwselbasb  16347  pwsvscafval  16353  pwssca  16355  pwssnf1o  16357  imassca  16378  imasvsca  16379  imasle  16382  xpslem  16432  xpssca  16437  xpsvsca  16438  isacs2  16512  homffval  16548  comfffval  16556  oppchomfval  16572  oppccofval  16574  oppccatid  16577  monfval  16590  oppcmon  16596  sectffval  16608  invffval  16616  rescbas  16687  reschom  16688  rescco  16690  fullsubc  16708  isfunc  16722  isfuncd  16723  idfu2nd  16735  idfu1st  16737  cofu1st  16741  cofu2nd  16743  fucco  16820  fucid  16829  invfuc  16832  initoval  16845  termoval  16846  homafval  16877  arwval  16891  coafval  16912  coapm  16919  setccatid  16932  catchomfval  16946  catccofval  16948  catccatid  16950  elestrchom  16966  estrccatid  16970  xpcbas  17017  xpchomfval  17018  xpccofval  17021  1stf1  17031  1stf2  17032  2ndf1  17034  2ndf2  17035  prf1  17039  prf2fval  17040  evlf2  17057  evlf1  17059  curf1fval  17063  curf11  17065  curf12  17066  curf1cl  17067  curf2  17068  curf2cl  17070  hof2fval  17094  yonedalem4a  17114  yonedalem4c  17116  yonedalem3  17119  yonedainv  17120  isdrs  17133  ispos  17146  pltfval  17158  lubfval  17177  lubeldm  17180  lubval  17183  glbfval  17190  glbeldm  17193  glbval  17196  clatlem  17310  clatlubcl2  17312  clatglbcl2  17314  odupos  17334  oduglb  17338  odumeet  17339  odulub  17340  odujoin  17341  ipolt  17358  ipopos  17359  isacs4lem  17367  isdlat  17392  plusffval  17446  issstrmgm  17451  gsumvalx  17469  gsumval  17470  issubmnd  17517  ress0g  17518  ismhm  17536  0mhm  17557  submacs  17564  pwsdiagmhm  17568  gsumz  17573  frmdplusg  17590  grpsubfval  17663  mulgfval  17741  mulgval  17742  issubg  17790  0subg  17815  subgacs  17825  nsgacs  17826  nmznsg  17834  eqgfval  17838  isghm  17856  gicen  17915  isga  17919  subgga  17928  orbstafun  17939  orbstaval  17940  orbsta  17941  orbsta2  17942  cntzfval  17948  cntzval  17949  oppgplusfval  17973  symgplusg  18004  symg2bas  18013  cayleylem2  18028  psgnfval  18115  odinf  18175  dfod2  18176  pgpfi1  18205  pgp0  18206  sylow1lem2  18209  sylow3lem6  18242  lsmfval  18248  lsmvalx  18249  oppglsm  18252  pj1fval  18302  efglem  18324  efgtf  18330  efgrelexlemb  18358  efgcpbllemb  18363  frgpeccl  18369  frgpmhm  18373  vrgpval  18375  frgpuplem  18380  frgpupf  18381  frgpupval  18382  frgpup1  18383  frgpup3lem  18385  frgpnabllem2  18472  iscygodd  18485  prmcyg  18490  lt6abl  18491  gsumval3a  18499  gsumval3  18503  gsumzres  18505  gsumzcl2  18506  gsumzf1o  18508  gsumzaddlem  18516  gsumzadd  18517  gsumzsplit  18522  gsummptshft  18531  gsumzmhm  18532  gsumzoppg  18539  gsumzinv  18540  gsummptfidminv  18542  gsumsub  18543  gsumpt  18556  gsummptf1o  18557  gsum2dlem1  18564  gsum2dlem2  18565  gsum2d  18566  gsum2d2lem  18567  fsfnn0gsumfsffz  18574  nn0gsumfz  18575  gsummptnn0fz  18577  dprdfid  18612  dprdfinv  18614  dprdfadd  18615  dprdfeq0  18617  dmdprdsplitlem  18632  dpjidcl  18653  ablfacrplem  18660  ablfacrp  18661  ablfacrp2  18662  ablfac1a  18664  ablfac1b  18665  ablfac1c  18666  ablfac1eu  18668  pgpfaclem2  18677  ablfaclem2  18681  ablfaclem3  18682  mgpplusg  18689  mgpress  18696  issrg  18703  ring1ne0  18787  gsumdixp  18805  pwsmgp  18814  opprmulfval  18821  dvdsrval  18841  isunit  18853  unitgrp  18863  unitlinv  18873  unitrinv  18874  dvrfval  18880  isdrng2  18955  drngmcl  18958  drngid2  18961  issubrg  18978  subrgugrp  18997  isabv  19017  staffval  19045  islmod  19065  scaffval  19079  lcomfsupp  19101  mptscmfsupp0  19126  rmodislmod  19129  lssset  19132  islss  19133  lsssn0  19146  lssacs  19168  lspfval  19174  lspval  19176  lspcl  19177  lspuni0  19211  lss0v  19217  0lmhm  19241  lmhmvsca  19246  islbs  19277  islbs3  19358  lbsextlem1  19361  lbsextlem3  19363  lbsextlem4  19364  lbsext  19366  rsp1  19427  drngnidl  19432  2idlval  19436  qusrhm  19440  isnzr2  19466  isnzr2hash  19467  0ring  19473  01eq0ring  19475  0ring01eqbi  19476  rrgval  19490  rrgsupp  19494  aspval  19531  psrbas  19581  psrelbas  19582  psrplusg  19584  psrmulr  19587  psrvscafval  19593  psrvscacl  19596  psr0lid  19598  psrlidm  19606  psrridm  19607  resspsradd  19619  resspsrmul  19620  resspsrvsca  19621  mvrval2  19625  mplsubglem  19637  mpllsslem  19638  mplsubrglem  19642  mpladd  19645  mplmul  19646  ressmpladd  19660  ressmplmul  19661  ressmplvsca  19662  mplmon  19666  mplmonmul  19667  mplcoe1  19668  opsrle  19678  opsrtoslem2  19687  mplmon2  19695  evlslem4  19710  psrbagev1  19712  evlslem2  19714  evlslem3  19716  evlsval2  19722  coe1sfi  19785  coe1fsupp  19786  mptcoe1fsupp  19787  coe1ae0  19788  ressply1add  19802  ressply1mul  19803  ressply1vsca  19804  gsumply1subr  19806  psropprmul  19810  coe1tmmul2fv  19850  coe1pwmulfv  19852  ply1coe  19868  cply1coe0  19871  cply1coe0bi  19872  gsummoncoe1  19876  evls1fval  19886  evls1val  19887  evls1rhmlem  19888  evls1sca  19890  evls1gsumadd  19891  evls1gsummul  19892  evl1val  19895  evl1fval1lem  19896  fveval1fvcl  19899  evl1sca  19900  evl1var  19902  evl1addd  19907  evl1subd  19908  evl1muld  19909  evl1expd  19911  pf1f  19916  pf1mpf  19918  pf1ind  19921  evl1gsummul  19926  expghm  20046  zrhrhmb  20061  zlmvsca  20072  zntoslem  20106  znfi  20109  znunithash  20114  psgnghm  20127  psgnghm2  20128  psgnevpmb  20134  ipffval  20197  ocvfval  20214  ocvval  20215  elocv  20216  thlbas  20244  thlle  20245  thlleval  20246  thloc  20247  pjfval  20254  pjdm  20255  pjpm  20256  isobs  20268  frlmbas  20303  frlmbasf  20308  frlmvscafval  20313  frlmsslss2  20318  frlmip  20321  frlmphllem  20323  uvcvval  20329  uvcvvcl  20330  frlmssuvc2  20338  frlmsslsp  20339  ellspd  20345  elfilspd  20346  islinds2  20356  islindf4  20381  mamures  20400  mndvcl  20401  mamucl  20411  mamuvs1  20415  mamuvs2  20416  matbas2d  20433  matecl  20435  mamumat1cl  20449  mat1comp  20450  mamulid  20451  mamurid  20452  mat1ov  20459  matsc  20461  mat1dimelbas  20482  mat1dimmul  20487  mat1f1o  20489  dmatval  20503  dmatmulcl  20511  scmatval  20515  scmatscmiddistr  20519  mavmulcl  20558  1mavmul  20559  marrepfval  20571  marrepeval  20574  marepvfval  20576  submafval  20590  mdetfval  20597  mdetunilem9  20631  mdetuni0  20632  m2detleiblem3  20640  m2detleiblem4  20641  minmar1fval  20657  minmar1eval  20660  symgmatr01  20666  gsummatr01lem3  20669  gsummatr01  20671  smadiadetlem1a  20675  smadiadetlem3  20680  invrvald  20688  cpmat  20721  mat2pmatfval  20735  mat2pmatbas  20738  decpmatfsupp  20781  decpmatmulsumfsupp  20785  pmatcollpw3lem  20795  pmatcollpw3fi1lem2  20799  pm2mpval  20807  mply1topmatcl  20817  chmatval  20841  chpmatfval  20842  chfacffsupp  20868  chfacfscmul0  20870  chfacfscmulfsupp  20871  chfacfpmmul0  20874  chfacfpmmulfsupp  20875  cpmidpmatlem2  20883  cpmadumatpolylem1  20893  imastopn  21731  uzrest  21908  tmdgsum2  22107  distgp  22110  indistgp  22111  snclseqg  22126  tsmsval  22141  tsms0  22152  tsmsres  22154  tsmsadd  22157  tsmsxplem1  22163  tsmsxplem2  22164  ussid  22271  isusp  22272  ressust  22275  cnextucn  22314  prdsxmetlem  22380  nrmmetd  22586  nmfval  22600  tngds  22659  tngnm  22662  tngngp2  22663  tngngpd  22664  tngngp  22665  tngngp3  22667  nmo0  22746  xrrest  22817  climcncf  22910  cphsubrglem  23183  cphcjcl  23189  tchex  23222  ipcau2  23239  cmsss  23353  rrxip  23384  minveclem4a  23407  minveclem4  23409  mbflimsup  23641  mbflim  23643  mdegfval  24030  mdegleb  24032  mdegldg  24034  deg1val  24064  uc1pval  24107  mon1pval  24109  q1pval  24121  r1pval  24124  ply1remlem  24130  ply1rem  24131  fta1glem1  24133  fta1glem2  24134  fta1blem  24136  ig1pval  24140  elqaalem3  24284  ulmcau  24357  ulmdvlem1  24362  ulmdvlem3  24364  mbfulm  24368  itgulm  24370  dchrplusg  25180  dchrmulid2  25185  dchrinvcl  25186  dchrptlem2  25198  dchrptlem3  25199  dchrsum2  25201  sumdchr2  25203  dchr2sum  25206  axtgcont1  25575  tglowdim1  25603  tgldimor  25605  tgldim0eq  25606  iscgrgd  25616  isismt  25637  tglnfn  25650  tglnunirn  25651  tglngval  25654  legval  25687  ishlg  25705  hlcgrex  25719  hlcgreulem  25720  mirval  25758  midexlem  25795  israg  25800  perpln1  25813  perpln2  25814  isperp  25815  ishpg  25859  midf  25876  ismidb  25878  lmif  25885  islmib  25887  iscgra  25909  isinag  25937  isleag  25941  iseqlg  25955  ttgval  25963  ttgitvval  25970  setsvtx  26135  uhgrunop  26178  incistruhgr  26182  upgrunop  26222  umgrunop  26224  usgriedgleord  26329  uspgredgleord  26334  uhgr0vsize0  26341  lfuhgr1v0e  26356  uhgrspanop  26398  upgrspanop  26399  umgrspanop  26400  usgrspanop  26401  uhgrspan1lem1  26402  upgrres1lem1  26411  usgredgffibi  26426  fusgredgfi  26427  usgr1v0e  26428  nbgr2vtx1edg  26456  nbuhgr2vtx1edgb  26458  nbfusgrlevtxm1  26489  nbfusgrlevtxm2  26490  uvtx01vtx  26512  cplgr1vlem  26547  cplgr1v  26548  cusgrsize2inds  26571  cusgrfilem3  26575  sizusglecusg  26581  fusgrmaxsize  26582  vtxdgfval  26585  vtxdun  26599  vtxd0nedgb  26606  p1evtxdeqlem  26630  p1evtxdeq  26631  p1evtxdp1  26632  usgrvd0nedg  26651  vtxdginducedm1lem1  26657  vtxdginducedm1lem4  26660  vtxdginducedm1  26661  vtxdginducedm1fi  26662  finsumvtxdg2ssteplem4  26666  rusgrnumwrdl2  26704  wksfval  26727  iswlkg  26731  wlkonprop  26776  wlkp1lem3  26794  wlkp1lem8  26799  wlkp1  26800  wksonproplem  26823  wwlks  26950  wwlksnon  26967  wspthsnon  26968  clwwlk  27120  0wlkonlem2  27286  conngrv2edg  27362  eupthp1  27383  eupth2eucrct  27384  eupthvdres  27402  eupth2lem3  27403  eupth2lemb  27404  3cyclfrgrrn  27455  frgrwopreglem1  27481  frgrwopreg1  27487  imsmetlem  27867  dipfval  27879  sspval  27900  islno  27930  nmooval  27940  nmounbseqi  27954  nmobndseqi  27956  0ofval  27964  0oval  27965  ajfval  27986  isph  27999  phpar  28001  ajval  28039  ubthlem1  28048  ubthlem2  28049  minvecolem4b  28056  minvecolem4  28058  minvecolem5  28059  hlex  28076  ressplusf  29969  ressnm  29970  oppglt  29973  ressprs  29974  oduprs  29975  inftmrel  30053  isinftm  30054  gsumvsca1  30101  gsummptres  30103  ress1r  30108  rdivmuldivd  30110  ringinvval  30111  dvrcan5  30112  ofldlt1  30132  resvsca  30149  mdetpmtr1  30208  pstmfval  30258  ordtrest2NEW  30288  ordtconnlem1  30289  fsumcvg4  30315  pl1cn  30320  qqhval  30337  sibf0  30715  sitgclg  30723  sitgaddlemb  30729  eulerpartlemgvv  30757  afsval  31068  mrsubfval  31722  mrsubcv  31724  mrsubff  31726  mrsubrn  31727  elmrsubrn  31734  msubfval  31738  msubff  31744  mpstval  31749  elmpst  31750  msrval  31752  mstaval  31758  msubvrs  31774  mclsssvlem  31776  mclsval  31777  mclsind  31784  mppsval  31786  climlec3  31935  sdclem2  33843  sdclem1  33844  caures  33861  heiborlem3  33917  heibor  33925  grpokerinj  33997  rngoi  34003  dvrunz  34058  isdrngo1  34060  isdrngo2  34062  isrngohom  34069  idlval  34117  isidl  34118  0idl  34129  0rngo  34131  divrngidl  34132  smprngopr  34156  igenval  34165  lshpset  34752  lsatset  34764  lcvfbr  34794  islfl  34834  lfl0f  34843  lfl1  34844  lfladd0l  34848  lflnegl  34850  lflvscl  34851  lflvsdi1  34852  lflvsdi2  34853  lflvsdi2a  34854  lflvsass  34855  lfl0sc  34856  lflsc0N  34857  lfl1sc  34858  lkr0f  34868  lkrsc  34871  eqlkr2  34874  ldualvbase  34900  ldualfvadd  34902  ldualvaddval  34905  ldualsca  34906  ldualfvs  34910  ldualvsval  34912  isopos  34954  cmtfvalN  34984  cvrfval  35042  pats  35059  glbconN  35151  llnset  35279  lplnset  35303  lvolset  35346  lineset  35512  isline  35513  pointsetN  35515  psubspset  35518  ispsubsp  35519  pmapval  35531  paddfval  35571  paddval  35572  pclfvalN  35663  pclvalN  35664  polfvalN  35678  polvalN  35679  psubclsetN  35710  ispsubclN  35711  watvalN  35767  lhpset  35769  lautset  35856  islaut  35857  pautsetN  35872  ispautN  35873  ldilset  35883  ltrnset  35892  dilsetN  35928  cdleme26e  36134  cdleme26eALTN  36136  cdleme26fALTN  36137  cdleme26f  36138  cdleme26f2ALTN  36139  cdleme26f2  36140  cdlemefs32sn1aw  36189  cdleme43fsv1snlem  36195  cdleme41sn3a  36208  cdleme32a  36216  cdleme40m  36242  cdleme40n  36243  cdleme42b  36253  tgrpbase  36521  tgrpopr  36522  istendo  36535  tendopl  36551  tendo02  36562  erngbase  36576  erngfplus  36577  erngfmul  36580  erngbase-rN  36584  erngfplus-rN  36585  erngfmul-rN  36588  cdlemk36  36688  cdlemkid  36711  dvasca  36781  dvavbase  36788  dvafvadd  36789  dvafvsca  36791  diafval  36806  diaval  36807  dvhsca  36857  dvhvbase  36862  dvhfvadd  36866  dvhfvsca  36875  docafvalN  36897  docavalN  36898  djafvalN  36909  djavalN  36910  dibfval  36916  dibopelvalN  36918  dibopelval2  36920  dibelval3  36922  diblsmopel  36946  dicfval  36950  dicval  36951  cdlemn11a  36982  dihvalcqpre  37010  dihopelvalcpre  37023  dihord6apre  37031  dihpN  37111  dochfval  37125  dochval  37126  djhfval  37172  djhval  37173  islpolN  37258  lpolconN  37262  dochpolN  37265  lcfrlem9  37325  lcd0vvalN  37388  mapdval  37403  mapd1o  37423  mapdunirnN  37425  mapdhval  37499  mapdhval0  37500  hvmapfval  37534  hvmapval  37535  hdmap1fval  37571  hdmap1vallem  37572  hgmapfval  37661  hlhilset  37709  hlhilbase  37711  hlhilplus  37712  hlhilvsca  37722  hlhilip  37723  hlhilnvl  37725  hlhillsm  37731  hlhillcs  37733  islssfgi  38137  pwssplit4  38154  frlmpwfi  38163  mendplusgfval  38250  mendmulrfval  38252  mendvscafval  38255  subrgacs  38265  sdrgacs  38266  cntzsdrg  38267  idomrootle  38268  idomodle  38269  deg1mhm  38280  dvgrat  39005  uzmptshftfval  39039  climexp  40311  climinf  40312  climneg  40316  climdivf  40318  climconstmpt  40364  climresmpt  40365  climsubmpt  40366  fnlimfvre  40380  limsupvaluz  40414  limsupequzmpt2  40424  climuzlem  40449  climisp  40452  climxrrelem  40455  climxrre  40456  limsupgtlem  40483  liminflelimsupuz  40491  liminfgelimsupuz  40494  liminfequzmpt2  40497  liminfvaluz  40498  limsupvaluz3  40504  climliminflimsupd  40507  liminfreuzlem  40508  liminfltlem  40510  liminflimsupclim  40513  xlimclim2lem  40539  climxlim2  40546  sge0isum  41117  sge0uzfsumgt  41134  sge0seq  41136  meaiunlelem  41158  caragendifcl  41204  omeiunle  41207  omeiunltfirp  41209  carageniuncl  41213  caragensal  41215  opnssborel  41325  smflimlem6  41460  smfpimcc  41490  smflimmpt  41492  smflimsuplem4  41505  smflimsuplem6  41507  smflimsuplem8  41509  smfliminflem  41512  upwlksfval  42278  isupwlkg  42280  ismgmhm  42345  issubmgm2  42352  submgmacs  42366  copisnmnd  42371  0ringdif  42432  rnghmval  42453  isrnghm  42454  c0snmgmhm  42476  c0snmhm  42477  zrrnghm  42479  zlidlring  42490  cznrng  42517  cznnring  42518  rngchomfvalALTV  42546  rngccofvalALTV  42549  rngccatidALTV  42551  ringchomfvalALTV  42609  ringccofvalALTV  42612  ringccatidALTV  42614  rngcrescrhm  42647  rngcrescrhmALTV  42665  ofaddmndmap  42684  suppmptcfin  42722  mptcfsupp  42723  dmatALTbas  42752  lcoop  42762  linccl  42765  lcosn0  42771  lincvalsc0  42772  lcoc0  42773  linc0scn0  42774  linc1  42776  lincscmcl  42783  islinindfis  42800  lincext1  42805  lincext2  42806  lindslinindimp2lem2  42810  lindslinindimp2lem3  42811  lindsrng01  42819  snlindsntorlem  42821  snlindsntor  42822  ldepspr  42824  lincresunit1  42828  lincresunit2  42829