Theorem fvexi 6513

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

Syntax hints:   = wceq 1507   ∈ wcel 2050  Vcvv 3415  ‘cfv 6188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-nul 5067

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-v 3417  df-sbc 3682  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-sn 4442  df-pr 4444  df-uni 4713  df-iota 6152  df-fv 6196

This theorem is referenced by:  mptfvmpt  6816  ovex  7008  mapfienlem1  8663  climle  14857  climsup  14887  iserabs  15030  isumshft  15054  explecnv  15080  prodfclim1  15109  ressbas  16410  ressbas2  16411  ressid  16415  ressval3d  16417  topnid  16565  prdsplusg  16587  prdsmulr  16588  prdsvsca  16589  prdsip  16590  prdsle  16591  prdsds  16593  prdshom  16596  prdsco  16597  pwselbasb  16617  pwsvscafval  16623  pwssca  16625  pwssnf1o  16627  imassca  16648  imasvsca  16649  imasle  16652  xpslem  16702  xpssca  16707  xpsvsca  16708  isacs2  16782  homffval  16818  comfffval  16826  oppchomfval  16842  oppccofval  16844  oppccatid  16847  monfval  16860  oppcmon  16866  sectffval  16878  invffval  16886  rescbas  16957  reschom  16958  rescco  16960  fullsubc  16978  isfunc  16992  isfuncd  16993  idfu2nd  17005  idfu1st  17007  cofu1st  17011  cofu2nd  17013  fucco  17090  fucid  17099  invfuc  17102  initoval  17115  termoval  17116  homafval  17147  arwval  17161  coafval  17182  coapm  17189  setccatid  17202  catchomfval  17216  catccofval  17218  catccatid  17220  elestrchom  17236  estrccatid  17240  xpcbas  17286  xpchomfval  17287  xpccofval  17290  1stf1  17300  1stf2  17301  2ndf1  17303  2ndf2  17304  prf1  17308  prf2fval  17309  evlf2  17326  evlf1  17328  curf1fval  17332  curf11  17334  curf12  17335  curf1cl  17336  curf2  17337  curf2cl  17339  hof2fval  17363  yonedalem4a  17383  yonedalem4c  17385  yonedalem3  17388  yonedainv  17389  isdrs  17402  ispos  17415  pltfval  17427  lubfval  17446  lubeldm  17449  lubval  17452  glbfval  17459  glbeldm  17462  glbval  17465  clatlem  17579  clatlubcl2  17581  clatglbcl2  17583  odupos  17603  oduglb  17607  odumeet  17608  odulub  17609  odujoin  17610  ipolt  17627  ipopos  17628  isacs4lem  17636  isdlat  17661  plusffval  17715  issstrmgm  17720  gsumvalx  17738  gsumval  17739  issubmnd  17786  ress0g  17787  ismhm  17805  0mhm  17826  submacs  17833  pwsdiagmhm  17837  gsumz  17842  frmdplusg  17860  grpinvfval  17929  grpsubfval  17934  grpsubfvalALT  17935  mulgfval  18013  mulgfvalALT  18014  mulgval  18015  issubg  18063  0subg  18088  subgacs  18098  nsgacs  18099  nmznsg  18107  eqgfval  18111  isghm  18129  gicen  18188  isga  18192  subgga  18201  orbstafun  18212  orbstaval  18213  orbsta  18214  cntzfval  18221  cntzval  18222  oppgplusfval  18247  symgplusg  18278  symg2bas  18287  cayleylem2  18302  psgnfval  18390  odfval  18422  odinf  18451  dfod2  18452  pgpfi1  18481  pgp0  18482  sylow1lem2  18485  sylow3lem6  18518  lsmfval  18524  lsmvalx  18525  oppglsm  18528  pj1fval  18578  efglem  18600  efgtf  18606  efgrelexlemb  18636  efgcpbllemb  18641  frgpeccl  18647  frgpmhm  18651  vrgpval  18653  frgpuplem  18658  frgpupf  18659  frgpupval  18660  frgpup1  18661  frgpup3lem  18663  frgpnabllem2  18750  iscygodd  18763  prmcyg  18768  lt6abl  18769  gsumval3a  18777  gsumval3  18781  gsumzres  18783  gsumzcl2  18784  gsumzf1o  18786  gsumzaddlem  18794  gsumzadd  18795  gsumzsplit  18800  gsummptshft  18809  gsumzmhm  18810  gsumzoppg  18817  gsumzinv  18818  gsummptfidminv  18820  gsumsub  18821  gsumpt  18835  gsummptf1o  18836  gsum2dlem1  18843  gsum2dlem2  18844  gsum2d  18845  gsum2d2lem  18846  fsfnn0gsumfsffz  18853  nn0gsumfz  18854  gsummptnn0fz  18856  dprdfid  18889  dprdfinv  18891  dprdfadd  18892  dprdfeq0  18894  dmdprdsplitlem  18909  dpjidcl  18930  ablfacrplem  18937  ablfacrp  18938  ablfacrp2  18939  ablfac1a  18941  ablfac1b  18942  ablfac1c  18943  ablfac1eu  18945  pgpfaclem2  18954  ablfaclem2  18958  ablfaclem3  18959  mgpplusg  18966  mgpress  18973  issrg  18980  ring1ne0  19064  gsumdixp  19082  pwsmgp  19091  opprmulfval  19098  dvdsrval  19118  isunit  19130  unitgrp  19140  unitlinv  19150  unitrinv  19151  dvrfval  19157  isdrng2  19235  drngmcl  19238  drngid2  19241  issubrg  19258  subrgugrp  19277  subrgacs  19301  sdrgacs  19302  cntzsdrg  19303  subdrgint  19304  isabv  19312  staffval  19340  islmod  19360  scaffval  19374  lcomfsupp  19396  mptscmfsupp0  19421  rmodislmod  19424  lssset  19427  islss  19428  lsssn0  19441  lssacs  19461  lspfval  19467  lspval  19469  lspcl  19470  lspuni0  19504  lss0v  19510  0lmhm  19534  lmhmvsca  19539  islbs  19570  islbs3  19649  lbsextlem1  19652  lbsextlem3  19654  lbsextlem4  19655  lbsext  19657  rsp1  19718  2idlval  19727  qusrhm  19731  isnzr2  19757  isnzr2hash  19758  0ring  19764  01eq0ring  19766  0ring01eqbi  19767  rrgval  19781  rrgsupp  19785  aspval  19822  psrbas  19872  psrelbas  19873  psrplusg  19875  psrmulr  19878  psrvscafval  19884  psrvscacl  19887  psr0lid  19889  psrlidm  19897  psrridm  19898  resspsradd  19910  resspsrmul  19911  resspsrvsca  19912  mvrval2  19916  mplsubglem  19928  mpllsslem  19929  mplsubrglem  19933  mpladd  19936  mplmul  19937  ressmpladd  19951  ressmplmul  19952  ressmplvsca  19953  mplmon  19957  mplmonmul  19958  mplcoe1  19959  opsrle  19969  opsrtoslem2  19978  mplmon2  19986  evlslem4  20001  psrbagev1  20003  evlslem2  20005  evlslem3  20007  evlsval2  20013  mhpval  20039  coe1sfi  20084  coe1fsupp  20085  mptcoe1fsupp  20086  coe1ae0  20087  ressply1add  20101  ressply1mul  20102  ressply1vsca  20103  gsumply1subr  20105  psropprmul  20109  coe1tmmul2fv  20149  coe1pwmulfv  20151  ply1coe  20167  cply1coe0  20170  cply1coe0bi  20171  gsummoncoe1  20175  evls1fval  20185  evls1val  20186  evls1rhmlem  20187  evls1sca  20189  evls1gsumadd  20190  evls1gsummul  20191  evl1val  20194  evl1fval1lem  20195  fveval1fvcl  20198  evl1sca  20199  evl1var  20201  evl1addd  20206  evl1subd  20207  evl1muld  20208  evl1expd  20210  pf1f  20215  pf1mpf  20217  pf1ind  20220  evl1gsummul  20225  expghm  20345  zrhrhmb  20360  zlmvsca  20371  zntoslem  20405  znfi  20408  znunithash  20413  psgnghm  20426  psgnghm2  20427  psgnevpmb  20433  ipffval  20494  ocvfval  20512  ocvval  20513  elocv  20514  thlbas  20542  thlle  20543  thlleval  20544  thloc  20545  pjfval  20552  pjdm  20553  pjpm  20554  isobs  20566  frlmbas  20601  frlmbasf  20606  frlmvscafval  20612  frlmvscavalb  20616  frlmsslss2  20621  frlmip  20624  frlmphllem  20626  uvcvval  20632  uvcvvcl  20633  frlmssuvc2  20641  frlmsslsp  20642  ellspd  20648  elfilspd  20649  islinds2  20659  islindf4  20684  mamures  20703  mndvcl  20704  mamucl  20714  mamuvs1  20718  mamuvs2  20719  matbas2d  20736  matecl  20738  mamumat1cl  20752  mat1comp  20753  mamulid  20754  mamurid  20755  mat1ov  20761  matsc  20763  mat1dimelbas  20784  mat1dimmul  20789  mat1f1o  20791  dmatval  20805  dmatmulcl  20813  scmatval  20817  scmatscmiddistr  20821  mavmulcl  20860  1mavmul  20861  marrepfval  20873  marrepeval  20876  marepvfval  20878  submafval  20892  mdetfval  20899  mdetunilem9  20933  mdetuni0  20934  m2detleiblem3  20942  m2detleiblem4  20943  minmar1fval  20959  minmar1eval  20962  symgmatr01  20967  gsummatr01lem3  20970  gsummatr01  20972  smadiadetlem1a  20976  smadiadetlem3  20981  invrvald  20989  cpmat  21021  mat2pmatfval  21035  mat2pmatbas  21038  decpmatfsupp  21081  decpmatmulsumfsupp  21085  pmatcollpw3lem  21095  pmatcollpw3fi1lem2  21099  pm2mpval  21107  mply1topmatcl  21117  chmatval  21141  chpmatfval  21142  chfacffsupp  21168  chfacfscmul0  21170  chfacfscmulfsupp  21171  chfacfpmmul0  21174  chfacfpmmulfsupp  21175  cpmidpmatlem2  21183  cpmadumatpolylem1  21193  imastopn  22032  uzrest  22209  tmdgsum2  22408  distgp  22411  indistgp  22412  snclseqg  22427  tsmsval  22442  tsms0  22453  tsmsres  22455  tsmsadd  22458  tsmsxplem1  22464  tsmsxplem2  22465  ussid  22572  isusp  22573  ressust  22576  cnextucn  22615  prdsxmetlem  22681  nrmmetd  22887  nmfval  22901  tngds  22960  tngnm  22963  tngngp2  22964  tngngpd  22965  tngngp  22966  tngngp3  22968  nmo0  23047  xrrest  23118  climcncf  23211  cphsubrglem  23484  cphcjcl  23490  tcphex  23523  ipcau2  23540  cmsss  23657  rrxip  23696  minveclem4a  23736  minveclem4  23738  mbflimsup  23970  mbflim  23972  mdegfval  24359  mdegleb  24361  mdegldg  24363  deg1val  24393  uc1pval  24436  mon1pval  24438  q1pval  24450  r1pval  24453  ply1remlem  24459  ply1rem  24460  fta1glem1  24462  fta1glem2  24463  fta1blem  24465  ig1pval  24469  elqaalem3  24613  ulmcau  24686  ulmdvlem1  24691  ulmdvlem3  24693  mbfulm  24697  itgulm  24699  dchrplusg  25525  dchrmulid2  25530  dchrinvcl  25531  dchrptlem2  25543  dchrptlem3  25544  dchrsum2  25546  sumdchr2  25548  dchr2sum  25551  axtgcont1  25956  tgjustc1  25963  tgjustc2  25964  tglowdim1  25988  tgldimor  25990  tgldim0eq  25991  iscgrgd  26001  isismt  26022  tglnfn  26035  tglnunirn  26036  tglngval  26039  legval  26072  ishlg  26090  hlcgrex  26104  hlcgreulem  26105  mirval  26143  midexlem  26180  israg  26185  perpln1  26198  perpln2  26199  isperp  26200  ishpg  26247  midf  26264  ismidb  26266  lmif  26273  islmib  26275  iscgra  26297  isinag  26327  isleag  26336  iseqlg  26356  ttgval  26364  ttgitvval  26371  setsvtx  26523  uhgrunop  26563  incistruhgr  26567  upgrunop  26607  umgrunop  26609  usgriedgleord  26713  uspgredgleord  26717  uhgr0vsize0  26724  lfuhgr1v0e  26739  uhgrspanop  26781  upgrspanop  26782  umgrspanop  26783  usgrspanop  26784  uhgrspan1lem1  26785  upgrres1lem1  26794  usgredgffibi  26809  fusgredgfi  26810  usgr1v0e  26811  nbgr2vtx1edg  26835  nbuhgr2vtx1edgb  26837  nbfusgrlevtxm1  26862  nbfusgrlevtxm2  26863  uvtx01vtx  26882  cplgr1vlem  26914  cplgr1v  26915  cusgrsize2inds  26938  cusgrfilem3  26942  sizusglecusg  26948  fusgrmaxsize  26949  vtxdgfval  26952  vtxdun  26966  vtxd0nedgb  26973  p1evtxdeqlem  26997  p1evtxdeq  26998  p1evtxdp1  26999  usgrvd0nedg  27018  vtxdginducedm1lem1  27024  vtxdginducedm1lem4  27027  vtxdginducedm1  27028  vtxdginducedm1fi  27029  finsumvtxdg2ssteplem4  27033  rusgrnumwrdl2  27071  wksfval  27094  iswlkg  27098  wlkonprop  27142  wlkp1lem3  27163  wlkp1lem8  27168  wlkp1  27169  wksonproplem  27194  wwlks  27321  wwlksnon  27337  wspthsnon  27338  clwwlk  27489  0wlkonlem2  27648  conngrv2edg  27724  eupthp1  27746  eupth2eucrct  27747  eupthvdres  27765  eupth2lem3  27766  eupth2lemb  27767  3cyclfrgrrn  27820  frgrwopreglem1  27846  frgrwopreg1  27852  imsmetlem  28244  dipfval  28256  sspval  28277  islno  28307  nmooval  28317  nmounbseqi  28331  nmobndseqi  28333  0ofval  28341  0oval  28342  ajfval  28363  isph  28376  phpar  28378  ajval  28416  ubthlem1  28425  ubthlem2  28426  minvecolem4b  28433  minvecolem4  28435  minvecolem5  28436  hlex  28453  ressplusf  30375  ressnm  30376  oppglt  30379  ressprs  30380  oduprs  30381  inftmrel  30481  isinftm  30482  gsumvsca1  30531  gsummptres  30535  ress1r  30545  rdivmuldivd  30547  ringinvval  30548  dvrcan5  30549  rmfsupp2  30551  ofldlt1  30571  resvsca  30588  quslmod  30608  fply1  30610  islinds5  30611  ellspds  30612  linds2eq  30618  dimval  30636  dimvalfi  30637  lvecdim0  30640  mdetpmtr1  30736  pstmfval  30786  ordtrest2NEW  30816  ordtconnlem1  30817  fsumcvg4  30843  pl1cn  30848  qqhval  30865  sibf0  31243  sitgclg  31251  sitgaddlemb  31257  eulerpartlemgvv  31285  afsval  31596  mrsubfval  32281  mrsubcv  32283  mrsubff  32285  mrsubrn  32286  elmrsubrn  32293  msubfval  32297  msubff  32303  mpstval  32308  elmpst  32309  msrval  32311  mstaval  32317  msubvrs  32333  mclsssvlem  32335  mclsval  32336  mclsind  32343  mppsval  32345  climlec3  32491  sdclem2  34465  sdclem1  34466  caures  34483  heiborlem3  34539  heibor  34547  grpokerinj  34619  rngoi  34625  dvrunz  34680  isdrngo1  34682  isdrngo2  34684  isrngohom  34691  idlval  34739  isidl  34740  0idl  34751  0rngo  34753  divrngidl  34754  smprngopr  34778  igenval  34787  lshpset  35565  lsatset  35577  lcvfbr  35607  islfl  35647  lfl0f  35656  lfl1  35657  lfladd0l  35661  lflnegl  35663  lflvscl  35664  lflvsdi1  35665  lflvsdi2  35666  lflvsdi2a  35667  lflvsass  35668  lfl0sc  35669  lflsc0N  35670  lfl1sc  35671  lkr0f  35681  lkrsc  35684  eqlkr2  35687  ldualvbase  35713  ldualfvadd  35715  ldualvaddval  35718  ldualsca  35719  ldualfvs  35723  ldualvsval  35725  isopos  35767  cmtfvalN  35797  cvrfval  35855  pats  35872  glbconN  35964  llnset  36092  lplnset  36116  lvolset  36159  lineset  36325  isline  36326  pointsetN  36328  psubspset  36331  ispsubsp  36332  pmapval  36344  paddfval  36384  paddval  36385  pclfvalN  36476  pclvalN  36477  polfvalN  36491  polvalN  36492  psubclsetN  36523  ispsubclN  36524  watvalN  36580  lhpset  36582  lautset  36669  islaut  36670  pautsetN  36685  ispautN  36686  ldilset  36696  ltrnset  36705  dilsetN  36740  cdleme26e  36946  cdleme26eALTN  36948  cdleme26fALTN  36949  cdleme26f  36950  cdleme26f2ALTN  36951  cdleme26f2  36952  cdlemefs32sn1aw  37001  cdleme43fsv1snlem  37007  cdleme41sn3a  37020  cdleme32a  37028  cdleme40m  37054  cdleme40n  37055  cdleme42b  37065  tgrpbase  37333  tgrpopr  37334  istendo  37347  tendopl  37363  tendo02  37374  erngbase  37388  erngfplus  37389  erngfmul  37392  erngbase-rN  37396  erngfplus-rN  37397  erngfmul-rN  37400  cdlemk36  37500  cdlemkid  37523  dvasca  37593  dvavbase  37600  dvafvadd  37601  dvafvsca  37603  diafval  37618  diaval  37619  dvhsca  37669  dvhvbase  37674  dvhfvadd  37678  dvhfvsca  37687  docafvalN  37709  docavalN  37710  djafvalN  37721  djavalN  37722  dibfval  37728  dibopelvalN  37730  dibopelval2  37732  dibelval3  37734  diblsmopel  37758  dicfval  37762  dicval  37763  cdlemn11a  37794  dihvalcqpre  37822  dihopelvalcpre  37835  dihord6apre  37843  dihpN  37923  dochfval  37937  dochval  37938  djhfval  37984  djhval  37985  islpolN  38070  lpolconN  38074  dochpolN  38077  lcfrlem9  38137  lcd0vvalN  38200  mapdval  38215  mapd1o  38235  mapdunirnN  38237  mapdhval  38311  mapdhval0  38312  hvmapfval  38346  hvmapval  38347  hdmap1fval  38383  hdmap1vallem  38384  hgmapfval  38473  hlhilset  38521  hlhilbase  38523  hlhilplus  38524  hlhilvsca  38534  hlhilip  38535  hlhilnvl  38537  hlhillsm  38543  hlhillcs  38545  frlmfielbas  38582  islssfgi  39074  pwssplit4  39091  frlmpwfi  39100  mendplusgfval  39187  mendmulrfval  39189  mendvscafval  39192  idomrootle  39197  idomodle  39198  deg1mhm  39209  2nsgsimpgd  40042  prmgrpsimpgd  40055  ablsimpgprmd  40056  dvgrat  40066  uzmptshftfval  40100  climexp  41323  climinf  41324  climneg  41328  climdivf  41330  climconstmpt  41376  climresmpt  41377  climsubmpt  41378  fnlimfvre  41392  limsupvaluz  41426  limsupequzmpt2  41436  climuzlem  41461  climisp  41464  climxrrelem  41467  climxrre  41468  limsupgtlem  41495  liminflelimsupuz  41503  liminfgelimsupuz  41506  liminfequzmpt2  41509  liminfvaluz  41510  limsupvaluz3  41516  climliminflimsupd  41519  liminfreuzlem  41520  liminfltlem  41522  liminflimsupclim  41525  liminflbuz2  41533  liminfpnfuz  41534  xlimclim2lem  41557  climxlim2  41564  sge0isum  42146  sge0uzfsumgt  42163  sge0seq  42165  meaiunlelem  42187  caragendifcl  42233  omeiunle  42236  omeiunltfirp  42238  carageniuncl  42242  caragensal  42244  opnssborel  42354  smflimlem6  42489  smfpimcc  42519  smflimmpt  42521  smflimsuplem4  42534  smflimsuplem6  42536  smflimsuplem8  42538  smfliminflem  42541  isomuspgrlem2  43372  ushrisomgr  43380  upwlksfval  43384  isupwlkg  43386  ismgmhm  43424  issubmgm2  43431  submgmacs  43445  copisnmnd  43450  0ringdif  43511  rnghmval  43532  isrnghm  43533  c0snmgmhm  43555  c0snmhm  43556  zrrnghm  43558  zlidlring  43569  cznrng  43596  cznnring  43597  rngchomfvalALTV  43625  rngccofvalALTV  43628  rngccatidALTV  43630  ringchomfvalALTV  43688  ringccofvalALTV  43691  ringccatidALTV  43693  rngcrescrhm  43726  rngcrescrhmALTV  43744  ofaddmndmap  43762  suppmptcfin  43799  mptcfsupp  43800  dmatALTbas  43829  lcoop  43839  linccl  43842  lcosn0  43848  lincvalsc0  43849  lcoc0  43850  linc0scn0  43851  linc1  43853  lincscmcl  43860  islinindfis  43877  lincext1  43882  lincext2  43883  lindslinindimp2lem2  43887  lindslinindimp2lem3  43888  lindsrng01  43896  snlindsntorlem  43898  snlindsntor  43899  ldepspr  43901  lincresunit1  43905  lincresunit2  43906  lines  44092  line  44093  rrxlines  44094  sphere  44108  rrxsphere  44109