Theorem fvexi 6731

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

Syntax hints:   = wceq 1543   ∈ wcel 2110  Vcvv 3408  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-nul 5199

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-sn 4542  df-pr 4544  df-uni 4820  df-iota 6338  df-fv 6388

This theorem is referenced by:  mptfvmpt  7044  ovex  7246  mapfienlem1  9021  climle  15201  climsup  15233  iserabs  15379  isumshft  15403  explecnv  15429  prodfclim1  15457  ressbas  16790  ressbas2  16791  ressid  16796  ressval3d  16798  topnid  16940  prdsplusg  16963  prdsmulr  16964  prdsvsca  16965  prdsip  16966  prdsle  16967  prdsds  16969  prdshom  16972  prdsco  16973  pwselbasb  16993  pwsvscafval  16999  pwssca  17001  pwssnf1o  17003  imassca  17024  imasvsca  17025  imasle  17028  xpsrnbas  17076  xpssca  17081  xpsvsca  17082  isacs2  17156  homffval  17193  comfffval  17201  oppchomfval  17217  oppchomfvalOLD  17218  oppccofval  17220  oppccatid  17223  monfval  17237  oppcmon  17243  sectffval  17255  invffval  17263  rescbas  17334  reschom  17335  rescco  17337  resccoOLD  17338  fullsubc  17356  isfunc  17370  isfuncd  17371  idfu2nd  17383  idfu1st  17385  cofu1st  17389  cofu2nd  17391  fucco  17471  fucid  17480  invfuc  17483  initoval  17499  termoval  17500  homafval  17535  arwval  17549  coafval  17570  coapm  17577  setccatid  17590  catchomfval  17608  catccofval  17610  catccatid  17612  elestrchom  17635  estrccatid  17639  xpcbas  17685  xpchomfval  17686  xpccofval  17689  1stf1  17699  1stf2  17700  2ndf1  17702  2ndf2  17703  prf1  17707  prf2fval  17708  evlf2  17726  evlf1  17728  curf1fval  17732  curf11  17734  curf12  17735  curf1cl  17736  curf2  17737  curf2cl  17739  hof2fval  17763  yonedalem4a  17783  yonedalem4c  17785  yonedalem3  17788  yonedainv  17789  isdrs  17808  ispos  17821  odupos  17834  pltfval  17837  lubfval  17856  lubeldm  17859  lubval  17862  glbfval  17869  glbeldm  17872  glbval  17875  odulub  17913  odujoin  17914  oduglb  17915  odumeet  17916  clatlem  18008  clatlubcl2  18010  clatglbcl2  18012  isdlat  18028  ipolt  18041  ipopos  18042  isacs4lem  18050  plusffval  18120  issstrmgm  18125  gsumvalx  18148  gsumval  18149  issubmnd  18200  ress0g  18201  ismhm  18220  0subm  18244  0mhm  18246  submacs  18253  pwsdiagmhm  18257  gsumz  18262  frmdplusg  18281  efmndplusg  18307  efmndmgm  18312  smndex1mgm  18334  grpinvfval  18406  grpsubfval  18411  grpsubfvalALT  18412  mulgfval  18490  mulgfvalALT  18491  mulgval  18492  issubg  18543  0subg  18568  subgacs  18577  nsgacs  18578  nmznsg  18584  eqgfval  18592  isghm  18622  gicen  18681  isga  18685  subgga  18694  orbstafun  18705  orbstaval  18706  orbsta  18707  cntzfval  18714  cntzval  18715  oppgplusfval  18740  symg2bas  18785  symgvalstruct  18789  cayleylem2  18805  psgnfval  18892  odfval  18924  odinf  18954  dfod2  18955  pgpfi1  18984  pgp0  18985  sylow1lem2  18988  sylow3lem6  19021  lsmfval  19027  lsmvalx  19028  oppglsm  19031  pj1fval  19084  efglem  19106  efgrelexlemb  19140  efgcpbllemb  19145  frgpeccl  19151  frgpmhm  19155  vrgpval  19157  frgpuplem  19162  frgpupf  19163  frgpupval  19164  frgpup1  19165  frgpup3lem  19167  frgpnabllem2  19259  iscygodd  19272  prmcyg  19279  lt6abl  19280  gsumval3a  19288  gsumval3  19292  gsumzres  19294  gsumzcl2  19295  gsumzf1o  19297  gsumreidx  19302  gsumzaddlem  19306  gsumzadd  19307  gsumzsplit  19312  gsummptshft  19321  gsumzmhm  19322  gsumzoppg  19329  gsumzinv  19330  gsummptfidminv  19332  gsumsub  19333  gsumpt  19347  gsummptf1o  19348  gsum2dlem1  19355  gsum2dlem2  19356  gsum2d  19357  gsum2d2lem  19358  gsumxp2  19365  fsfnn0gsumfsffz  19368  nn0gsumfz  19369  gsummptnn0fz  19371  dprdfid  19404  dprdfinv  19406  dprdfadd  19407  dprdfeq0  19409  dmdprdsplitlem  19424  dpjidcl  19445  ablfacrplem  19452  ablfacrp  19453  ablfacrp2  19454  ablfac1a  19456  ablfac1b  19457  ablfac1c  19458  ablfac1eu  19460  pgpfaclem2  19469  ablfaclem2  19473  ablfaclem3  19474  2nsgsimpgd  19489  prmgrpsimpgd  19501  ablsimpgprmd  19502  mgpplusg  19508  mgpress  19515  issrg  19522  ring1ne0  19609  gsumdixp  19627  pwsmgp  19636  opprmulfval  19643  dvdsrval  19663  isunit  19675  unitgrp  19685  unitlinv  19695  unitrinv  19696  dvrfval  19702  isdrng2  19777  drngmcl  19780  drngid2  19783  issubrg  19800  subrgugrp  19819  subrgacs  19844  sdrgacs  19845  cntzsdrg  19846  subdrgint  19847  isabv  19855  staffval  19883  islmod  19903  scaffval  19917  lcomfsupp  19939  mptscmfsupp0  19964  rmodislmod  19967  lssset  19970  islss  19971  lsssn0  19984  lssacs  20004  lspfval  20010  lspval  20012  lspcl  20013  lspuni0  20047  lss0v  20053  0lmhm  20077  lmhmvsca  20082  islbs  20113  islbs3  20192  lbsextlem1  20195  lbsextlem3  20197  lbsextlem4  20198  lbsext  20200  rsp1  20262  2idlval  20271  qusrhm  20275  isnzr2  20301  isnzr2hash  20302  0ring  20308  01eq0ring  20310  0ring01eqbi  20311  rrgval  20325  rrgsupp  20329  expghm  20462  zrhrhmb  20477  zlmvsca  20488  zntoslem  20521  znfi  20524  znunithash  20529  psgnghm  20542  psgnghm2  20543  psgnevpmb  20549  ipffval  20610  ocvfval  20628  ocvval  20629  elocv  20630  thlbas  20658  thlle  20659  thlleval  20660  thloc  20661  pjfval  20668  pjdm  20669  pjpm  20670  isobs  20682  frlmbas  20717  frlmbasf  20722  frlmvscafval  20728  frlmvscavalb  20732  frlmsslss2  20737  frlmip  20740  uvcvval  20748  uvcvvcl  20749  frlmssuvc2  20757  frlmsslsp  20758  ellspd  20764  elfilspd  20765  islinds2  20775  islindf4  20800  aspval  20832  psrbas  20903  psrelbas  20904  psrplusg  20906  psrmulr  20909  psrvscafval  20915  psrvscacl  20918  psr0lid  20920  psrlidm  20928  psrridm  20929  resspsradd  20941  resspsrmul  20942  resspsrvsca  20943  mvrval2  20947  mplsubglem  20961  mpllsslem  20962  mplsubrglem  20966  mpladd  20969  mplmul  20971  ressmpladd  20986  ressmplmul  20987  ressmplvsca  20988  mplmon  20992  mplmonmul  20993  mplcoe1  20994  opsrle  21004  opsrtoslem2  21013  mplmon2  21019  evlslem4  21034  psrbagev1  21035  psrbagev1OLD  21036  evlslem2  21039  evlslem3  21040  evlsval2  21047  selvval  21078  mhpval  21080  ismhp3  21083  coe1sfi  21134  coe1fsupp  21135  mptcoe1fsupp  21136  coe1ae0  21137  ressply1add  21151  ressply1mul  21152  ressply1vsca  21153  gsumply1subr  21155  psropprmul  21159  coe1tmmul2fv  21199  coe1pwmulfv  21201  ply1coe  21217  cply1coe0  21220  cply1coe0bi  21221  gsummoncoe1  21225  evls1fval  21235  evls1val  21236  evls1rhmlem  21237  evls1sca  21239  evls1gsumadd  21240  evls1gsummul  21241  evl1val  21245  evl1fval1lem  21246  fveval1fvcl  21249  evl1sca  21250  evl1var  21252  evl1addd  21257  evl1subd  21258  evl1muld  21259  evl1expd  21261  pf1f  21266  pf1mpf  21268  pf1ind  21271  evl1gsummul  21276  mamures  21289  mndvcl  21290  mamucl  21298  mamuvs1  21302  mamuvs2  21303  matbas2d  21320  matecl  21322  mamumat1cl  21336  mat1comp  21337  mamulid  21338  mamurid  21339  mat1ov  21345  matsc  21347  mat1dimelbas  21368  mat1dimmul  21373  mat1f1o  21375  dmatval  21389  dmatmulcl  21397  scmatval  21401  scmatscmiddistr  21405  mavmulcl  21444  1mavmul  21445  marrepfval  21457  marrepeval  21460  marepvfval  21462  submafval  21476  mdetfval  21483  mdetunilem9  21517  mdetuni0  21518  m2detleiblem3  21526  m2detleiblem4  21527  minmar1fval  21543  minmar1eval  21546  symgmatr01  21551  gsummatr01lem3  21554  gsummatr01  21556  smadiadetlem1a  21560  smadiadetlem3  21565  invrvald  21573  cpmat  21606  mat2pmatfval  21620  mat2pmatbas  21623  decpmatfsupp  21666  decpmatmulsumfsupp  21670  pmatcollpw3lem  21680  pmatcollpw3fi1lem2  21684  pm2mpval  21692  mply1topmatcl  21702  chmatval  21726  chpmatfval  21727  chfacffsupp  21753  chfacfscmul0  21755  chfacfscmulfsupp  21756  chfacfpmmul0  21759  chfacfpmmulfsupp  21760  cpmidpmatlem2  21768  cpmadumatpolylem1  21778  imastopn  22617  uzrest  22794  tmdgsum2  22993  distgp  22996  indistgp  22997  snclseqg  23013  tsmsval  23028  tsms0  23039  tsmsres  23041  tsmsxplem1  23050  tsmsxplem2  23051  ussid  23158  isusp  23159  ressust  23161  cnextucn  23200  prdsxmetlem  23266  nrmmetd  23472  nmfval  23486  tngds  23546  tngnm  23549  tngngp2  23550  tngngpd  23551  tngngp  23552  tngngp3  23554  nmo0  23633  xrrest  23704  climcncf  23797  cphsubrglem  24074  cphcjcl  24080  tcphex  24114  ipcau2  24131  cmsss  24248  rrxip  24287  minveclem4a  24327  minveclem4  24329  mbflimsup  24563  mbflim  24565  mdegfval  24960  mdegleb  24962  mdegldg  24964  deg1val  24994  uc1pval  25037  mon1pval  25039  q1pval  25051  r1pval  25054  ply1remlem  25060  ply1rem  25061  fta1glem1  25063  fta1glem2  25064  fta1blem  25066  ig1pval  25070  elqaalem3  25214  ulmcau  25287  ulmdvlem1  25292  ulmdvlem3  25294  mbfulm  25298  itgulm  25300  dchrplusg  26128  dchrmulid2  26133  dchrinvcl  26134  dchrptlem2  26146  dchrptlem3  26147  dchrsum2  26149  sumdchr2  26151  dchr2sum  26154  axtgcont1  26559  tgjustc1  26566  tgjustc2  26567  tglowdim1  26591  tgldimor  26593  tgldim0eq  26594  iscgrgd  26604  isismt  26625  tglnfn  26638  tglnunirn  26639  tglngval  26642  legval  26675  ishlg  26693  hlcgrex  26707  hlcgreulem  26708  mirval  26746  midexlem  26783  israg  26788  perpln1  26801  perpln2  26802  isperp  26803  ishpg  26850  midf  26867  ismidb  26869  lmif  26876  islmib  26878  iscgra  26900  isinag  26929  isleag  26938  iseqlg  26958  ttgval  26966  ttgitvval  26973  setsvtx  27126  uhgrunop  27166  incistruhgr  27170  upgrunop  27210  umgrunop  27212  usgriedgleord  27316  uspgredgleord  27320  uhgr0vsize0  27327  lfuhgr1v0e  27342  uhgrspanop  27384  upgrspanop  27385  umgrspanop  27386  usgrspanop  27387  uhgrspan1lem1  27388  upgrres1lem1  27397  usgredgffibi  27412  fusgredgfi  27413  usgr1v0e  27414  nbgr2vtx1edg  27438  nbuhgr2vtx1edgb  27440  nbfusgrlevtxm1  27465  nbfusgrlevtxm2  27466  uvtx01vtx  27485  cplgr1vlem  27517  cplgr1v  27518  cusgrsize2inds  27541  cusgrfilem3  27545  sizusglecusg  27551  fusgrmaxsize  27552  vtxdgfval  27555  vtxdun  27569  vtxd0nedgb  27576  p1evtxdeqlem  27600  p1evtxdeq  27601  p1evtxdp1  27602  usgrvd0nedg  27621  vtxdginducedm1lem1  27627  vtxdginducedm1lem4  27630  vtxdginducedm1  27631  vtxdginducedm1fi  27632  finsumvtxdg2ssteplem4  27636  rusgrnumwrdl2  27674  wksfval  27697  iswlkg  27701  wlkonprop  27746  wlkp1lem3  27763  wlkp1lem8  27768  wlkp1  27769  wksonproplem  27792  wwlks  27919  wwlksnon  27935  wspthsnon  27936  clwwlk  28066  0wlkonlem2  28202  conngrv2edg  28278  eupthp1  28299  eupth2eucrct  28300  eupthvdres  28318  eupth2lem3  28319  eupth2lemb  28320  3cyclfrgrrn  28369  frgrwopreglem1  28395  frgrwopreg1  28401  imsmetlem  28771  dipfval  28783  sspval  28804  islno  28834  nmooval  28844  nmounbseqi  28858  nmobndseqi  28860  0ofval  28868  0oval  28869  ajfval  28890  isph  28903  phpar  28905  ajval  28942  ubthlem1  28951  ubthlem2  28952  minvecolem4b  28959  minvecolem4  28961  minvecolem5  28962  hlex  28979  ressplusf  30955  ressnm  30956  oppglt  30959  ressprs  30960  oduprs  30961  ismnt  30980  mgcval  30984  gsummptres  31031  gsummptres2  31032  gsumpart  31034  gsumhashmul  31035  inftmrel  31153  isinftm  31154  gsumvsca1  31198  ress1r  31205  rdivmuldivd  31207  ringinvval  31208  dvrcan5  31209  rmfsupp2  31211  ofldlt1  31231  resvsca  31248  quslmod  31268  islinds5  31277  ellspds  31278  elrsp  31283  linds2eq  31289  elringlsm  31295  lsmsnpridl  31300  grplsm0l  31305  qusima  31308  nsgmgc  31311  nsgqusf1o  31315  elrspunidl  31320  prmidl0  31340  idlsrgbas  31363  idlsrgplusg  31364  idlsrgmulr  31366  idlsrgtset  31367  rprmval  31378  fply1  31381  dimval  31400  dimvalfi  31401  lvecdim0  31404  mdetpmtr1  31487  rspectopn  31531  zarcls0  31532  zarcls  31538  zartopn  31539  zarmxt1  31544  rhmpreimacnlem  31548  rhmpreimacn  31549  pstmfval  31560  ordtrest2NEW  31587  ordtconnlem1  31588  fsumcvg4  31614  pl1cn  31619  qqhval  31636  sibf0  32013  sitgclg  32021  sitgaddlemb  32027  eulerpartlemgvv  32055  afsval  32363  pthhashvtx  32802  usgrcyclgt2v  32806  cusgr3cyclex  32811  acycgr2v  32825  cusgracyclt3v  32831  mrsubfval  33183  mrsubcv  33185  mrsubff  33187  mrsubrn  33188  elmrsubrn  33195  msubfval  33199  msubff  33205  mpstval  33210  elmpst  33211  msrval  33213  mstaval  33219  msubvrs  33235  mclsssvlem  33237  mclsval  33238  mclsind  33245  mppsval  33247  climlec3  33417  sdclem2  35637  sdclem1  35638  caures  35655  heiborlem3  35708  heibor  35716  grpokerinj  35788  rngoi  35794  dvrunz  35849  isdrngo1  35851  isdrngo2  35853  isrngohom  35860  idlval  35908  isidl  35909  0idl  35920  0rngo  35922  divrngidl  35923  smprngopr  35947  igenval  35956  lshpset  36729  lsatset  36741  lcvfbr  36771  islfl  36811  lfl0f  36820  lfl1  36821  lfladd0l  36825  lflnegl  36827  lflvscl  36828  lflvsdi1  36829  lflvsdi2  36830  lflvsdi2a  36831  lflvsass  36832  lfl0sc  36833  lflsc0N  36834  lfl1sc  36835  lkr0f  36845  lkrsc  36848  eqlkr2  36851  ldualvbase  36877  ldualfvadd  36879  ldualvaddval  36882  ldualsca  36883  ldualfvs  36887  ldualvsval  36889  isopos  36931  cmtfvalN  36961  cvrfval  37019  pats  37036  glbconN  37128  llnset  37256  lplnset  37280  lvolset  37323  lineset  37489  isline  37490  pointsetN  37492  psubspset  37495  ispsubsp  37496  pmapval  37508  paddfval  37548  paddval  37549  pclfvalN  37640  pclvalN  37641  polfvalN  37655  polvalN  37656  psubclsetN  37687  ispsubclN  37688  watvalN  37744  lhpset  37746  lautset  37833  islaut  37834  pautsetN  37849  ispautN  37850  ldilset  37860  ltrnset  37869  dilsetN  37904  cdleme26e  38110  cdleme26eALTN  38112  cdleme26fALTN  38113  cdleme26f  38114  cdleme26f2ALTN  38115  cdleme26f2  38116  cdlemefs32sn1aw  38165  cdleme43fsv1snlem  38171  cdleme41sn3a  38184  cdleme32a  38192  cdleme40m  38218  cdleme40n  38219  cdleme42b  38229  tgrpbase  38497  tgrpopr  38498  istendo  38511  tendopl  38527  tendo02  38538  erngbase  38552  erngfplus  38553  erngfmul  38556  erngbase-rN  38560  erngfplus-rN  38561  erngfmul-rN  38564  cdlemk36  38664  cdlemkid  38687  dvasca  38757  dvavbase  38764  dvafvadd  38765  dvafvsca  38767  diafval  38782  diaval  38783  dvhsca  38833  dvhvbase  38838  dvhfvadd  38842  dvhfvsca  38851  docafvalN  38873  docavalN  38874  djafvalN  38885  djavalN  38886  dibfval  38892  dibopelvalN  38894  dibopelval2  38896  dibelval3  38898  diblsmopel  38922  dicfval  38926  dicval  38927  cdlemn11a  38958  dihvalcqpre  38986  dihopelvalcpre  38999  dihord6apre  39007  dihpN  39087  dochfval  39101  dochval  39102  djhfval  39148  djhval  39149  islpolN  39234  lpolconN  39238  dochpolN  39241  lcfrlem9  39301  lcd0vvalN  39364  mapdval  39379  mapd1o  39399  mapdunirnN  39401  mapdhval  39475  mapdhval0  39476  hvmapfval  39510  hvmapval  39511  hdmap1fval  39547  hdmap1vallem  39548  hgmapfval  39637  hlhilset  39685  hlhilbase  39687  hlhilplus  39688  hlhilvsca  39698  hlhilip  39699  hlhilnvl  39701  hlhillsm  39707  hlhillcs  39709  frlmfielbas  39944  frlm0vald  39974  evlsval3  39982  evlsbagval  39985  fsuppind  39989  fsuppssind  39992  mhpind  39993  mhphf  39995  islssfgi  40600  pwssplit4  40617  frlmpwfi  40626  mendplusgfval  40713  mendmulrfval  40715  mendvscafval  40718  idomrootle  40723  idomodle  40724  deg1mhm  40735  mnringelbased  41508  mnring0g2d  41513  mnringmulrd  41514  mnringmulrcld  41519  dvgrat  41603  uzmptshftfval  41637  climexp  42821  climinf  42822  climneg  42826  climdivf  42828  climconstmpt  42874  climresmpt  42875  climsubmpt  42876  fnlimfvre  42890  limsupvaluz  42924  limsupequzmpt2  42934  climuzlem  42959  climisp  42962  climxrrelem  42965  climxrre  42966  limsupgtlem  42993  liminflelimsupuz  43001  liminfgelimsupuz  43004  liminfequzmpt2  43007  liminfvaluz  43008  limsupvaluz3  43014  climliminflimsupd  43017  liminfreuzlem  43018  liminfltlem  43020  liminflimsupclim  43023  liminflbuz2  43031  liminfpnfuz  43032  xlimclim2lem  43055  climxlim2  43062  sge0isum  43640  sge0uzfsumgt  43657  sge0seq  43659  meaiunlelem  43681  caragendifcl  43727  omeiunle  43730  omeiunltfirp  43732  carageniuncl  43736  caragensal  43738  opnssborel  43848  smflimlem6  43983  smfpimcc  44013  smflimmpt  44015  smflimsuplem4  44028  smflimsuplem6  44030  smflimsuplem8  44032  smfliminflem  44035  isomuspgrlem2  44958  ushrisomgr  44966  upwlksfval  44970  isupwlkg  44972  ismgmhm  45010  issubmgm2  45017  submgmacs  45031  copisnmnd  45036  0ringdif  45101  rnghmval  45122  isrnghm  45123  c0snmgmhm  45145  c0snmhm  45146  zrrnghm  45148  zlidlring  45159  cznrng  45186  cznnring  45187  rngchomfvalALTV  45215  rngccofvalALTV  45218  rngccatidALTV  45220  ringchomfvalALTV  45278  ringccofvalALTV  45281  ringccatidALTV  45283  rngcrescrhm  45316  rngcrescrhmALTV  45334  ofaddmndmap  45352  suppmptcfin  45388  mptcfsupp  45389  dmatALTbas  45415  lcoop  45425  linccl  45428  lcosn0  45434  lincvalsc0  45435  lcoc0  45436  linc0scn0  45437  linc1  45439  lincscmcl  45446  islinindfis  45463  lincext1  45468  lincext2  45469  lindslinindimp2lem2  45473  lindslinindimp2lem3  45474  lindsrng01  45482  snlindsntorlem  45484  snlindsntor  45485  ldepspr  45487  lincresunit1  45491  lincresunit2  45492  lines  45750  line  45751  rrxlines  45752  sphere  45766  rrxsphere  45767  functhinclem1  45995  thincciso  46003