Theorem fvexi 6686

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  Vcvv 3496  ‘cfv 6357

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-sn 4570  df-pr 4572  df-uni 4841  df-iota 6316  df-fv 6365

This theorem is referenced by:  mptfvmpt  6992  ovex  7191  mapfienlem1  8870  climle  14998  climsup  15028  iserabs  15172  isumshft  15196  explecnv  15222  prodfclim1  15251  ressbas  16556  ressbas2  16557  ressid  16561  ressval3d  16563  topnid  16711  prdsplusg  16733  prdsmulr  16734  prdsvsca  16735  prdsip  16736  prdsle  16737  prdsds  16739  prdshom  16742  prdsco  16743  pwselbasb  16763  pwsvscafval  16769  pwssca  16771  pwssnf1o  16773  imassca  16794  imasvsca  16795  imasle  16798  xpsrnbas  16846  xpssca  16851  xpsvsca  16852  isacs2  16926  homffval  16962  comfffval  16970  oppchomfval  16986  oppccofval  16988  oppccatid  16991  monfval  17004  oppcmon  17010  sectffval  17022  invffval  17030  rescbas  17101  reschom  17102  rescco  17104  fullsubc  17122  isfunc  17136  isfuncd  17137  idfu2nd  17149  idfu1st  17151  cofu1st  17155  cofu2nd  17157  fucco  17234  fucid  17243  invfuc  17246  initoval  17259  termoval  17260  homafval  17291  arwval  17305  coafval  17326  coapm  17333  setccatid  17346  catchomfval  17360  catccofval  17362  catccatid  17364  elestrchom  17380  estrccatid  17384  xpcbas  17430  xpchomfval  17431  xpccofval  17434  1stf1  17444  1stf2  17445  2ndf1  17447  2ndf2  17448  prf1  17452  prf2fval  17453  evlf2  17470  evlf1  17472  curf1fval  17476  curf11  17478  curf12  17479  curf1cl  17480  curf2  17481  curf2cl  17483  hof2fval  17507  yonedalem4a  17527  yonedalem4c  17529  yonedalem3  17532  yonedainv  17533  isdrs  17546  ispos  17559  pltfval  17571  lubfval  17590  lubeldm  17593  lubval  17596  glbfval  17603  glbeldm  17606  glbval  17609  clatlem  17723  clatlubcl2  17725  clatglbcl2  17727  odupos  17747  oduglb  17751  odumeet  17752  odulub  17753  odujoin  17754  ipolt  17771  ipopos  17772  isacs4lem  17780  isdlat  17805  plusffval  17860  issstrmgm  17865  gsumvalx  17888  gsumval  17889  issubmnd  17940  ress0g  17941  ismhm  17960  0subm  17984  0mhm  17986  submacs  17993  pwsdiagmhm  17997  gsumz  18002  frmdplusg  18021  efmndplusg  18047  efmndmgm  18052  smndex1mgm  18074  grpinvfval  18144  grpsubfval  18149  grpsubfvalALT  18150  mulgfval  18228  mulgfvalALT  18229  mulgval  18230  issubg  18281  0subg  18306  subgacs  18315  nsgacs  18316  nmznsg  18322  eqgfval  18330  isghm  18360  gicen  18419  isga  18423  subgga  18432  orbstafun  18443  orbstaval  18444  orbsta  18445  cntzfval  18452  cntzval  18453  oppgplusfval  18478  symg2bas  18523  symgvalstruct  18527  cayleylem2  18543  psgnfval  18630  odfval  18662  odinf  18692  dfod2  18693  pgpfi1  18722  pgp0  18723  sylow1lem2  18726  sylow3lem6  18759  lsmfval  18765  lsmvalx  18766  oppglsm  18769  pj1fval  18822  efglem  18844  efgtf  18850  efgrelexlemb  18878  efgcpbllemb  18883  frgpeccl  18889  frgpmhm  18893  vrgpval  18895  frgpuplem  18900  frgpupf  18901  frgpupval  18902  frgpup1  18903  frgpup3lem  18905  frgpnabllem2  18996  iscygodd  19009  prmcyg  19016  lt6abl  19017  gsumval3a  19025  gsumval3  19029  gsumzres  19031  gsumzcl2  19032  gsumzf1o  19034  gsumreidx  19039  gsumzaddlem  19043  gsumzadd  19044  gsumzsplit  19049  gsummptshft  19058  gsumzmhm  19059  gsumzoppg  19066  gsumzinv  19067  gsummptfidminv  19069  gsumsub  19070  gsumpt  19084  gsummptf1o  19085  gsum2dlem1  19092  gsum2dlem2  19093  gsum2d  19094  gsum2d2lem  19095  gsumxp2  19102  fsfnn0gsumfsffz  19105  nn0gsumfz  19106  gsummptnn0fz  19108  dprdfid  19141  dprdfinv  19143  dprdfadd  19144  dprdfeq0  19146  dmdprdsplitlem  19161  dpjidcl  19182  ablfacrplem  19189  ablfacrp  19190  ablfacrp2  19191  ablfac1a  19193  ablfac1b  19194  ablfac1c  19195  ablfac1eu  19197  pgpfaclem2  19206  ablfaclem2  19210  ablfaclem3  19211  2nsgsimpgd  19226  prmgrpsimpgd  19238  ablsimpgprmd  19239  mgpplusg  19245  mgpress  19252  issrg  19259  ring1ne0  19343  gsumdixp  19361  pwsmgp  19370  opprmulfval  19377  dvdsrval  19397  isunit  19409  unitgrp  19419  unitlinv  19429  unitrinv  19430  dvrfval  19436  isdrng2  19514  drngmcl  19517  drngid2  19520  issubrg  19537  subrgugrp  19556  subrgacs  19581  sdrgacs  19582  cntzsdrg  19583  subdrgint  19584  isabv  19592  staffval  19620  islmod  19640  scaffval  19654  lcomfsupp  19676  mptscmfsupp0  19701  rmodislmod  19704  lssset  19707  islss  19708  lsssn0  19721  lssacs  19741  lspfval  19747  lspval  19749  lspcl  19750  lspuni0  19784  lss0v  19790  0lmhm  19814  lmhmvsca  19819  islbs  19850  islbs3  19929  lbsextlem1  19932  lbsextlem3  19934  lbsextlem4  19935  lbsext  19937  rsp1  19999  2idlval  20008  qusrhm  20012  isnzr2  20038  isnzr2hash  20039  0ring  20045  01eq0ring  20047  0ring01eqbi  20048  rrgval  20062  rrgsupp  20066  aspval  20104  psrbas  20160  psrelbas  20161  psrplusg  20163  psrmulr  20166  psrvscafval  20172  psrvscacl  20175  psr0lid  20177  psrlidm  20185  psrridm  20186  resspsradd  20198  resspsrmul  20199  resspsrvsca  20200  mvrval2  20204  mplsubglem  20216  mpllsslem  20217  mplsubrglem  20221  mpladd  20224  mplmul  20225  ressmpladd  20240  ressmplmul  20241  ressmplvsca  20242  mplmon  20246  mplmonmul  20247  mplcoe1  20248  opsrle  20258  opsrtoslem2  20267  mplmon2  20275  evlslem4  20290  psrbagev1  20292  evlslem2  20294  evlslem3  20295  evlsval2  20302  selvval  20333  mhpval  20335  coe1sfi  20383  coe1fsupp  20384  mptcoe1fsupp  20385  coe1ae0  20386  ressply1add  20400  ressply1mul  20401  ressply1vsca  20402  gsumply1subr  20404  psropprmul  20408  coe1tmmul2fv  20448  coe1pwmulfv  20450  ply1coe  20466  cply1coe0  20469  cply1coe0bi  20470  gsummoncoe1  20474  evls1fval  20484  evls1val  20485  evls1rhmlem  20486  evls1sca  20488  evls1gsumadd  20489  evls1gsummul  20490  evl1val  20494  evl1fval1lem  20495  fveval1fvcl  20498  evl1sca  20499  evl1var  20501  evl1addd  20506  evl1subd  20507  evl1muld  20508  evl1expd  20510  pf1f  20515  pf1mpf  20517  pf1ind  20520  evl1gsummul  20525  expghm  20645  zrhrhmb  20660  zlmvsca  20671  zntoslem  20705  znfi  20708  znunithash  20713  psgnghm  20726  psgnghm2  20727  psgnevpmb  20733  ipffval  20794  ocvfval  20812  ocvval  20813  elocv  20814  thlbas  20842  thlle  20843  thlleval  20844  thloc  20845  pjfval  20852  pjdm  20853  pjpm  20854  isobs  20866  frlmbas  20901  frlmbasf  20906  frlmvscafval  20912  frlmvscavalb  20916  frlmsslss2  20921  frlmip  20924  uvcvval  20932  uvcvvcl  20933  frlmssuvc2  20941  frlmsslsp  20942  ellspd  20948  elfilspd  20949  islinds2  20959  islindf4  20984  mamures  21003  mndvcl  21004  mamucl  21012  mamuvs1  21016  mamuvs2  21017  matbas2d  21034  matecl  21036  mamumat1cl  21050  mat1comp  21051  mamulid  21052  mamurid  21053  mat1ov  21059  matsc  21061  mat1dimelbas  21082  mat1dimmul  21087  mat1f1o  21089  dmatval  21103  dmatmulcl  21111  scmatval  21115  scmatscmiddistr  21119  mavmulcl  21158  1mavmul  21159  marrepfval  21171  marrepeval  21174  marepvfval  21176  submafval  21190  mdetfval  21197  mdetunilem9  21231  mdetuni0  21232  m2detleiblem3  21240  m2detleiblem4  21241  minmar1fval  21257  minmar1eval  21260  symgmatr01  21265  gsummatr01lem3  21268  gsummatr01  21270  smadiadetlem1a  21274  smadiadetlem3  21279  invrvald  21287  cpmat  21319  mat2pmatfval  21333  mat2pmatbas  21336  decpmatfsupp  21379  decpmatmulsumfsupp  21383  pmatcollpw3lem  21393  pmatcollpw3fi1lem2  21397  pm2mpval  21405  mply1topmatcl  21415  chmatval  21439  chpmatfval  21440  chfacffsupp  21466  chfacfscmul0  21468  chfacfscmulfsupp  21469  chfacfpmmul0  21472  chfacfpmmulfsupp  21473  cpmidpmatlem2  21481  cpmadumatpolylem1  21491  imastopn  22330  uzrest  22507  tmdgsum2  22706  distgp  22709  indistgp  22710  snclseqg  22726  tsmsval  22741  tsms0  22752  tsmsres  22754  tsmsadd  22757  tsmsxplem1  22763  tsmsxplem2  22764  ussid  22871  isusp  22872  ressust  22875  cnextucn  22914  prdsxmetlem  22980  nrmmetd  23186  nmfval  23200  tngds  23259  tngnm  23262  tngngp2  23263  tngngpd  23264  tngngp  23265  tngngp3  23267  nmo0  23346  xrrest  23417  climcncf  23510  cphsubrglem  23783  cphcjcl  23789  tcphex  23822  ipcau2  23839  cmsss  23956  rrxip  23995  minveclem4a  24035  minveclem4  24037  mbflimsup  24269  mbflim  24271  mdegfval  24658  mdegleb  24660  mdegldg  24662  deg1val  24692  uc1pval  24735  mon1pval  24737  q1pval  24749  r1pval  24752  ply1remlem  24758  ply1rem  24759  fta1glem1  24761  fta1glem2  24762  fta1blem  24764  ig1pval  24768  elqaalem3  24912  ulmcau  24985  ulmdvlem1  24990  ulmdvlem3  24992  mbfulm  24996  itgulm  24998  dchrplusg  25825  dchrmulid2  25830  dchrinvcl  25831  dchrptlem2  25843  dchrptlem3  25844  dchrsum2  25846  sumdchr2  25848  dchr2sum  25851  axtgcont1  26256  tgjustc1  26263  tgjustc2  26264  tglowdim1  26288  tgldimor  26290  tgldim0eq  26291  iscgrgd  26301  isismt  26322  tglnfn  26335  tglnunirn  26336  tglngval  26339  legval  26372  ishlg  26390  hlcgrex  26404  hlcgreulem  26405  mirval  26443  midexlem  26480  israg  26485  perpln1  26498  perpln2  26499  isperp  26500  ishpg  26547  midf  26564  ismidb  26566  lmif  26573  islmib  26575  iscgra  26597  isinag  26626  isleag  26635  iseqlg  26655  ttgval  26663  ttgitvval  26670  setsvtx  26822  uhgrunop  26862  incistruhgr  26866  upgrunop  26906  umgrunop  26908  usgriedgleord  27012  uspgredgleord  27016  uhgr0vsize0  27023  lfuhgr1v0e  27038  uhgrspanop  27080  upgrspanop  27081  umgrspanop  27082  usgrspanop  27083  uhgrspan1lem1  27084  upgrres1lem1  27093  usgredgffibi  27108  fusgredgfi  27109  usgr1v0e  27110  nbgr2vtx1edg  27134  nbuhgr2vtx1edgb  27136  nbfusgrlevtxm1  27161  nbfusgrlevtxm2  27162  uvtx01vtx  27181  cplgr1vlem  27213  cplgr1v  27214  cusgrsize2inds  27237  cusgrfilem3  27241  sizusglecusg  27247  fusgrmaxsize  27248  vtxdgfval  27251  vtxdun  27265  vtxd0nedgb  27272  p1evtxdeqlem  27296  p1evtxdeq  27297  p1evtxdp1  27298  usgrvd0nedg  27317  vtxdginducedm1lem1  27323  vtxdginducedm1lem4  27326  vtxdginducedm1  27327  vtxdginducedm1fi  27328  finsumvtxdg2ssteplem4  27332  rusgrnumwrdl2  27370  wksfval  27393  iswlkg  27397  wlkonprop  27442  wlkp1lem3  27459  wlkp1lem8  27464  wlkp1  27465  wksonproplem  27488  wwlks  27615  wwlksnon  27631  wspthsnon  27632  clwwlk  27763  0wlkonlem2  27900  conngrv2edg  27976  eupthp1  27997  eupth2eucrct  27998  eupthvdres  28016  eupth2lem3  28017  eupth2lemb  28018  3cyclfrgrrn  28067  frgrwopreglem1  28093  frgrwopreg1  28099  imsmetlem  28469  dipfval  28481  sspval  28502  islno  28532  nmooval  28542  nmounbseqi  28556  nmobndseqi  28558  0ofval  28566  0oval  28567  ajfval  28588  isph  28601  phpar  28603  ajval  28640  ubthlem1  28649  ubthlem2  28650  minvecolem4b  28657  minvecolem4  28659  minvecolem5  28660  hlex  28677  ressplusf  30639  ressnm  30640  oppglt  30643  ressprs  30644  oduprs  30645  gsummptres  30692  inftmrel  30811  isinftm  30812  gsumvsca1  30856  ress1r  30862  rdivmuldivd  30864  ringinvval  30865  dvrcan5  30866  rmfsupp2  30868  ofldlt1  30888  resvsca  30905  quslmod  30925  fply1  30933  islinds5  30934  ellspds  30935  linds2eq  30943  lsmsnpridl  30950  dimval  31003  dimvalfi  31004  lvecdim0  31007  mdetpmtr1  31090  pstmfval  31138  ordtrest2NEW  31168  ordtconnlem1  31169  fsumcvg4  31195  pl1cn  31200  qqhval  31217  sibf0  31594  sitgclg  31602  sitgaddlemb  31608  eulerpartlemgvv  31636  afsval  31944  pthhashvtx  32376  usgrcyclgt2v  32380  cusgr3cyclex  32385  acycgr2v  32399  cusgracyclt3v  32405  mrsubfval  32757  mrsubcv  32759  mrsubff  32761  mrsubrn  32762  elmrsubrn  32769  msubfval  32773  msubff  32779  mpstval  32784  elmpst  32785  msrval  32787  mstaval  32793  msubvrs  32809  mclsssvlem  32811  mclsval  32812  mclsind  32819  mppsval  32821  climlec3  32967  sdclem2  35019  sdclem1  35020  caures  35037  heiborlem3  35093  heibor  35101  grpokerinj  35173  rngoi  35179  dvrunz  35234  isdrngo1  35236  isdrngo2  35238  isrngohom  35245  idlval  35293  isidl  35294  0idl  35305  0rngo  35307  divrngidl  35308  smprngopr  35332  igenval  35341  lshpset  36116  lsatset  36128  lcvfbr  36158  islfl  36198  lfl0f  36207  lfl1  36208  lfladd0l  36212  lflnegl  36214  lflvscl  36215  lflvsdi1  36216  lflvsdi2  36217  lflvsdi2a  36218  lflvsass  36219  lfl0sc  36220  lflsc0N  36221  lfl1sc  36222  lkr0f  36232  lkrsc  36235  eqlkr2  36238  ldualvbase  36264  ldualfvadd  36266  ldualvaddval  36269  ldualsca  36270  ldualfvs  36274  ldualvsval  36276  isopos  36318  cmtfvalN  36348  cvrfval  36406  pats  36423  glbconN  36515  llnset  36643  lplnset  36667  lvolset  36710  lineset  36876  isline  36877  pointsetN  36879  psubspset  36882  ispsubsp  36883  pmapval  36895  paddfval  36935  paddval  36936  pclfvalN  37027  pclvalN  37028  polfvalN  37042  polvalN  37043  psubclsetN  37074  ispsubclN  37075  watvalN  37131  lhpset  37133  lautset  37220  islaut  37221  pautsetN  37236  ispautN  37237  ldilset  37247  ltrnset  37256  dilsetN  37291  cdleme26e  37497  cdleme26eALTN  37499  cdleme26fALTN  37500  cdleme26f  37501  cdleme26f2ALTN  37502  cdleme26f2  37503  cdlemefs32sn1aw  37552  cdleme43fsv1snlem  37558  cdleme41sn3a  37571  cdleme32a  37579  cdleme40m  37605  cdleme40n  37606  cdleme42b  37616  tgrpbase  37884  tgrpopr  37885  istendo  37898  tendopl  37914  tendo02  37925  erngbase  37939  erngfplus  37940  erngfmul  37943  erngbase-rN  37947  erngfplus-rN  37948  erngfmul-rN  37951  cdlemk36  38051  cdlemkid  38074  dvasca  38144  dvavbase  38151  dvafvadd  38152  dvafvsca  38154  diafval  38169  diaval  38170  dvhsca  38220  dvhvbase  38225  dvhfvadd  38229  dvhfvsca  38238  docafvalN  38260  docavalN  38261  djafvalN  38272  djavalN  38273  dibfval  38279  dibopelvalN  38281  dibopelval2  38283  dibelval3  38285  diblsmopel  38309  dicfval  38313  dicval  38314  cdlemn11a  38345  dihvalcqpre  38373  dihopelvalcpre  38386  dihord6apre  38394  dihpN  38474  dochfval  38488  dochval  38489  djhfval  38535  djhval  38536  islpolN  38621  lpolconN  38625  dochpolN  38628  lcfrlem9  38688  lcd0vvalN  38751  mapdval  38766  mapd1o  38786  mapdunirnN  38788  mapdhval  38862  mapdhval0  38863  hvmapfval  38897  hvmapval  38898  hdmap1fval  38934  hdmap1vallem  38935  hgmapfval  39024  hlhilset  39072  hlhilbase  39074  hlhilplus  39075  hlhilvsca  39085  hlhilip  39086  hlhilnvl  39088  hlhillsm  39094  hlhillcs  39096  frlmfielbas  39146  islssfgi  39679  pwssplit4  39696  frlmpwfi  39705  mendplusgfval  39792  mendmulrfval  39794  mendvscafval  39797  idomrootle  39802  idomodle  39803  deg1mhm  39814  dvgrat  40651  uzmptshftfval  40685  climexp  41893  climinf  41894  climneg  41898  climdivf  41900  climconstmpt  41946  climresmpt  41947  climsubmpt  41948  fnlimfvre  41962  limsupvaluz  41996  limsupequzmpt2  42006  climuzlem  42031  climisp  42034  climxrrelem  42037  climxrre  42038  limsupgtlem  42065  liminflelimsupuz  42073  liminfgelimsupuz  42076  liminfequzmpt2  42079  liminfvaluz  42080  limsupvaluz3  42086  climliminflimsupd  42089  liminfreuzlem  42090  liminfltlem  42092  liminflimsupclim  42095  liminflbuz2  42103  liminfpnfuz  42104  xlimclim2lem  42127  climxlim2  42134  sge0isum  42716  sge0uzfsumgt  42733  sge0seq  42735  meaiunlelem  42757  caragendifcl  42803  omeiunle  42806  omeiunltfirp  42808  carageniuncl  42812  caragensal  42814  opnssborel  42924  smflimlem6  43059  smfpimcc  43089  smflimmpt  43091  smflimsuplem4  43104  smflimsuplem6  43106  smflimsuplem8  43108  smfliminflem  43111  isomuspgrlem2  44005  ushrisomgr  44013  upwlksfval  44017  isupwlkg  44019  ismgmhm  44057  issubmgm2  44064  submgmacs  44078  copisnmnd  44083  0ringdif  44148  rnghmval  44169  isrnghm  44170  c0snmgmhm  44192  c0snmhm  44193  zrrnghm  44195  zlidlring  44206  cznrng  44233  cznnring  44234  rngchomfvalALTV  44262  rngccofvalALTV  44265  rngccatidALTV  44267  ringchomfvalALTV  44325  ringccofvalALTV  44328  ringccatidALTV  44330  rngcrescrhm  44363  rngcrescrhmALTV  44381  ofaddmndmap  44399  suppmptcfin  44434  mptcfsupp  44435  dmatALTbas  44463  lcoop  44473  linccl  44476  lcosn0  44482  lincvalsc0  44483  lcoc0  44484  linc0scn0  44485  linc1  44487  lincscmcl  44494  islinindfis  44511  lincext1  44516  lincext2  44517  lindslinindimp2lem2  44521  lindslinindimp2lem3  44522  lindsrng01  44530  snlindsntorlem  44532  snlindsntor  44533  ldepspr  44535  lincresunit1  44539  lincresunit2  44540  lines  44725  line  44726  rrxlines  44727  sphere  44741  rrxsphere  44742