Theorem fvexi 6678

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

Syntax hints:   = wceq 1533   ∈ wcel 2110  Vcvv 3494  ‘cfv 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-sn 4561  df-pr 4563  df-uni 4832  df-iota 6308  df-fv 6357

This theorem is referenced by:  mptfvmpt  6984  ovex  7183  mapfienlem1  8862  climle  14990  climsup  15020  iserabs  15164  isumshft  15188  explecnv  15214  prodfclim1  15243  ressbas  16548  ressbas2  16549  ressid  16553  ressval3d  16555  topnid  16703  prdsplusg  16725  prdsmulr  16726  prdsvsca  16727  prdsip  16728  prdsle  16729  prdsds  16731  prdshom  16734  prdsco  16735  pwselbasb  16755  pwsvscafval  16761  pwssca  16763  pwssnf1o  16765  imassca  16786  imasvsca  16787  imasle  16790  xpsrnbas  16838  xpssca  16843  xpsvsca  16844  isacs2  16918  homffval  16954  comfffval  16962  oppchomfval  16978  oppccofval  16980  oppccatid  16983  monfval  16996  oppcmon  17002  sectffval  17014  invffval  17022  rescbas  17093  reschom  17094  rescco  17096  fullsubc  17114  isfunc  17128  isfuncd  17129  idfu2nd  17141  idfu1st  17143  cofu1st  17147  cofu2nd  17149  fucco  17226  fucid  17235  invfuc  17238  initoval  17251  termoval  17252  homafval  17283  arwval  17297  coafval  17318  coapm  17325  setccatid  17338  catchomfval  17352  catccofval  17354  catccatid  17356  elestrchom  17372  estrccatid  17376  xpcbas  17422  xpchomfval  17423  xpccofval  17426  1stf1  17436  1stf2  17437  2ndf1  17439  2ndf2  17440  prf1  17444  prf2fval  17445  evlf2  17462  evlf1  17464  curf1fval  17468  curf11  17470  curf12  17471  curf1cl  17472  curf2  17473  curf2cl  17475  hof2fval  17499  yonedalem4a  17519  yonedalem4c  17521  yonedalem3  17524  yonedainv  17525  isdrs  17538  ispos  17551  pltfval  17563  lubfval  17582  lubeldm  17585  lubval  17588  glbfval  17595  glbeldm  17598  glbval  17601  clatlem  17715  clatlubcl2  17717  clatglbcl2  17719  odupos  17739  oduglb  17743  odumeet  17744  odulub  17745  odujoin  17746  ipolt  17763  ipopos  17764  isacs4lem  17772  isdlat  17797  plusffval  17852  issstrmgm  17857  gsumvalx  17880  gsumval  17881  issubmnd  17932  ress0g  17933  ismhm  17952  0subm  17976  0mhm  17978  submacs  17985  pwsdiagmhm  17989  gsumz  17994  frmdplusg  18013  efmndplusg  18039  efmndmgm  18044  smndex1mgm  18066  grpinvfval  18136  grpsubfval  18141  grpsubfvalALT  18142  mulgfval  18220  mulgfvalALT  18221  mulgval  18222  issubg  18273  0subg  18298  subgacs  18307  nsgacs  18308  nmznsg  18314  eqgfval  18322  isghm  18352  gicen  18411  isga  18415  subgga  18424  orbstafun  18435  orbstaval  18436  orbsta  18437  cntzfval  18444  cntzval  18445  oppgplusfval  18470  symg2bas  18515  symgvalstruct  18519  cayleylem2  18535  psgnfval  18622  odfval  18654  odinf  18684  dfod2  18685  pgpfi1  18714  pgp0  18715  sylow1lem2  18718  sylow3lem6  18751  lsmfval  18757  lsmvalx  18758  oppglsm  18761  pj1fval  18814  efglem  18836  efgtf  18842  efgrelexlemb  18870  efgcpbllemb  18875  frgpeccl  18881  frgpmhm  18885  vrgpval  18887  frgpuplem  18892  frgpupf  18893  frgpupval  18894  frgpup1  18895  frgpup3lem  18897  frgpnabllem2  18988  iscygodd  19001  prmcyg  19008  lt6abl  19009  gsumval3a  19017  gsumval3  19021  gsumzres  19023  gsumzcl2  19024  gsumzf1o  19026  gsumreidx  19031  gsumzaddlem  19035  gsumzadd  19036  gsumzsplit  19041  gsummptshft  19050  gsumzmhm  19051  gsumzoppg  19058  gsumzinv  19059  gsummptfidminv  19061  gsumsub  19062  gsumpt  19076  gsummptf1o  19077  gsum2dlem1  19084  gsum2dlem2  19085  gsum2d  19086  gsum2d2lem  19087  gsumxp2  19094  fsfnn0gsumfsffz  19097  nn0gsumfz  19098  gsummptnn0fz  19100  dprdfid  19133  dprdfinv  19135  dprdfadd  19136  dprdfeq0  19138  dmdprdsplitlem  19153  dpjidcl  19174  ablfacrplem  19181  ablfacrp  19182  ablfacrp2  19183  ablfac1a  19185  ablfac1b  19186  ablfac1c  19187  ablfac1eu  19189  pgpfaclem2  19198  ablfaclem2  19202  ablfaclem3  19203  2nsgsimpgd  19218  prmgrpsimpgd  19230  ablsimpgprmd  19231  mgpplusg  19237  mgpress  19244  issrg  19251  ring1ne0  19335  gsumdixp  19353  pwsmgp  19362  opprmulfval  19369  dvdsrval  19389  isunit  19401  unitgrp  19411  unitlinv  19421  unitrinv  19422  dvrfval  19428  isdrng2  19506  drngmcl  19509  drngid2  19512  issubrg  19529  subrgugrp  19548  subrgacs  19573  sdrgacs  19574  cntzsdrg  19575  subdrgint  19576  isabv  19584  staffval  19612  islmod  19632  scaffval  19646  lcomfsupp  19668  mptscmfsupp0  19693  rmodislmod  19696  lssset  19699  islss  19700  lsssn0  19713  lssacs  19733  lspfval  19739  lspval  19741  lspcl  19742  lspuni0  19776  lss0v  19782  0lmhm  19806  lmhmvsca  19811  islbs  19842  islbs3  19921  lbsextlem1  19924  lbsextlem3  19926  lbsextlem4  19927  lbsext  19929  rsp1  19991  2idlval  20000  qusrhm  20004  isnzr2  20030  isnzr2hash  20031  0ring  20037  01eq0ring  20039  0ring01eqbi  20040  rrgval  20054  rrgsupp  20058  aspval  20096  psrbas  20152  psrelbas  20153  psrplusg  20155  psrmulr  20158  psrvscafval  20164  psrvscacl  20167  psr0lid  20169  psrlidm  20177  psrridm  20178  resspsradd  20190  resspsrmul  20191  resspsrvsca  20192  mvrval2  20196  mplsubglem  20208  mpllsslem  20209  mplsubrglem  20213  mpladd  20216  mplmul  20217  ressmpladd  20232  ressmplmul  20233  ressmplvsca  20234  mplmon  20238  mplmonmul  20239  mplcoe1  20240  opsrle  20250  opsrtoslem2  20259  mplmon2  20267  evlslem4  20282  psrbagev1  20284  evlslem2  20286  evlslem3  20287  evlsval2  20294  selvval  20325  mhpval  20327  coe1sfi  20375  coe1fsupp  20376  mptcoe1fsupp  20377  coe1ae0  20378  ressply1add  20392  ressply1mul  20393  ressply1vsca  20394  gsumply1subr  20396  psropprmul  20400  coe1tmmul2fv  20440  coe1pwmulfv  20442  ply1coe  20458  cply1coe0  20461  cply1coe0bi  20462  gsummoncoe1  20466  evls1fval  20476  evls1val  20477  evls1rhmlem  20478  evls1sca  20480  evls1gsumadd  20481  evls1gsummul  20482  evl1val  20486  evl1fval1lem  20487  fveval1fvcl  20490  evl1sca  20491  evl1var  20493  evl1addd  20498  evl1subd  20499  evl1muld  20500  evl1expd  20502  pf1f  20507  pf1mpf  20509  pf1ind  20512  evl1gsummul  20517  expghm  20637  zrhrhmb  20652  zlmvsca  20663  zntoslem  20697  znfi  20700  znunithash  20705  psgnghm  20718  psgnghm2  20719  psgnevpmb  20725  ipffval  20786  ocvfval  20804  ocvval  20805  elocv  20806  thlbas  20834  thlle  20835  thlleval  20836  thloc  20837  pjfval  20844  pjdm  20845  pjpm  20846  isobs  20858  frlmbas  20893  frlmbasf  20898  frlmvscafval  20904  frlmvscavalb  20908  frlmsslss2  20913  frlmip  20916  uvcvval  20924  uvcvvcl  20925  frlmssuvc2  20933  frlmsslsp  20934  ellspd  20940  elfilspd  20941  islinds2  20951  islindf4  20976  mamures  20995  mndvcl  20996  mamucl  21004  mamuvs1  21008  mamuvs2  21009  matbas2d  21026  matecl  21028  mamumat1cl  21042  mat1comp  21043  mamulid  21044  mamurid  21045  mat1ov  21051  matsc  21053  mat1dimelbas  21074  mat1dimmul  21079  mat1f1o  21081  dmatval  21095  dmatmulcl  21103  scmatval  21107  scmatscmiddistr  21111  mavmulcl  21150  1mavmul  21151  marrepfval  21163  marrepeval  21166  marepvfval  21168  submafval  21182  mdetfval  21189  mdetunilem9  21223  mdetuni0  21224  m2detleiblem3  21232  m2detleiblem4  21233  minmar1fval  21249  minmar1eval  21252  symgmatr01  21257  gsummatr01lem3  21260  gsummatr01  21262  smadiadetlem1a  21266  smadiadetlem3  21271  invrvald  21279  cpmat  21311  mat2pmatfval  21325  mat2pmatbas  21328  decpmatfsupp  21371  decpmatmulsumfsupp  21375  pmatcollpw3lem  21385  pmatcollpw3fi1lem2  21389  pm2mpval  21397  mply1topmatcl  21407  chmatval  21431  chpmatfval  21432  chfacffsupp  21458  chfacfscmul0  21460  chfacfscmulfsupp  21461  chfacfpmmul0  21464  chfacfpmmulfsupp  21465  cpmidpmatlem2  21473  cpmadumatpolylem1  21483  imastopn  22322  uzrest  22499  tmdgsum2  22698  distgp  22701  indistgp  22702  snclseqg  22718  tsmsval  22733  tsms0  22744  tsmsres  22746  tsmsadd  22749  tsmsxplem1  22755  tsmsxplem2  22756  ussid  22863  isusp  22864  ressust  22867  cnextucn  22906  prdsxmetlem  22972  nrmmetd  23178  nmfval  23192  tngds  23251  tngnm  23254  tngngp2  23255  tngngpd  23256  tngngp  23257  tngngp3  23259  nmo0  23338  xrrest  23409  climcncf  23502  cphsubrglem  23775  cphcjcl  23781  tcphex  23814  ipcau2  23831  cmsss  23948  rrxip  23987  minveclem4a  24027  minveclem4  24029  mbflimsup  24261  mbflim  24263  mdegfval  24650  mdegleb  24652  mdegldg  24654  deg1val  24684  uc1pval  24727  mon1pval  24729  q1pval  24741  r1pval  24744  ply1remlem  24750  ply1rem  24751  fta1glem1  24753  fta1glem2  24754  fta1blem  24756  ig1pval  24760  elqaalem3  24904  ulmcau  24977  ulmdvlem1  24982  ulmdvlem3  24984  mbfulm  24988  itgulm  24990  dchrplusg  25817  dchrmulid2  25822  dchrinvcl  25823  dchrptlem2  25835  dchrptlem3  25836  dchrsum2  25838  sumdchr2  25840  dchr2sum  25843  axtgcont1  26248  tgjustc1  26255  tgjustc2  26256  tglowdim1  26280  tgldimor  26282  tgldim0eq  26283  iscgrgd  26293  isismt  26314  tglnfn  26327  tglnunirn  26328  tglngval  26331  legval  26364  ishlg  26382  hlcgrex  26396  hlcgreulem  26397  mirval  26435  midexlem  26472  israg  26477  perpln1  26490  perpln2  26491  isperp  26492  ishpg  26539  midf  26556  ismidb  26558  lmif  26565  islmib  26567  iscgra  26589  isinag  26618  isleag  26627  iseqlg  26647  ttgval  26655  ttgitvval  26662  setsvtx  26814  uhgrunop  26854  incistruhgr  26858  upgrunop  26898  umgrunop  26900  usgriedgleord  27004  uspgredgleord  27008  uhgr0vsize0  27015  lfuhgr1v0e  27030  uhgrspanop  27072  upgrspanop  27073  umgrspanop  27074  usgrspanop  27075  uhgrspan1lem1  27076  upgrres1lem1  27085  usgredgffibi  27100  fusgredgfi  27101  usgr1v0e  27102  nbgr2vtx1edg  27126  nbuhgr2vtx1edgb  27128  nbfusgrlevtxm1  27153  nbfusgrlevtxm2  27154  uvtx01vtx  27173  cplgr1vlem  27205  cplgr1v  27206  cusgrsize2inds  27229  cusgrfilem3  27233  sizusglecusg  27239  fusgrmaxsize  27240  vtxdgfval  27243  vtxdun  27257  vtxd0nedgb  27264  p1evtxdeqlem  27288  p1evtxdeq  27289  p1evtxdp1  27290  usgrvd0nedg  27309  vtxdginducedm1lem1  27315  vtxdginducedm1lem4  27318  vtxdginducedm1  27319  vtxdginducedm1fi  27320  finsumvtxdg2ssteplem4  27324  rusgrnumwrdl2  27362  wksfval  27385  iswlkg  27389  wlkonprop  27434  wlkp1lem3  27451  wlkp1lem8  27456  wlkp1  27457  wksonproplem  27480  wwlks  27607  wwlksnon  27623  wspthsnon  27624  clwwlk  27755  0wlkonlem2  27892  conngrv2edg  27968  eupthp1  27989  eupth2eucrct  27990  eupthvdres  28008  eupth2lem3  28009  eupth2lemb  28010  3cyclfrgrrn  28059  frgrwopreglem1  28085  frgrwopreg1  28091  imsmetlem  28461  dipfval  28473  sspval  28494  islno  28524  nmooval  28534  nmounbseqi  28548  nmobndseqi  28550  0ofval  28558  0oval  28559  ajfval  28580  isph  28593  phpar  28595  ajval  28632  ubthlem1  28641  ubthlem2  28642  minvecolem4b  28649  minvecolem4  28651  minvecolem5  28652  hlex  28669  ressplusf  30632  ressnm  30633  oppglt  30636  ressprs  30637  oduprs  30638  gsummptres  30685  inftmrel  30804  isinftm  30805  gsumvsca1  30849  ress1r  30855  rdivmuldivd  30857  ringinvval  30858  dvrcan5  30859  rmfsupp2  30861  ofldlt1  30881  resvsca  30898  quslmod  30918  fply1  30926  islinds5  30927  ellspds  30928  linds2eq  30936  lsmsnpridl  30943  dimval  30996  dimvalfi  30997  lvecdim0  31000  mdetpmtr1  31083  pstmfval  31131  ordtrest2NEW  31161  ordtconnlem1  31162  fsumcvg4  31188  pl1cn  31193  qqhval  31210  sibf0  31587  sitgclg  31595  sitgaddlemb  31601  eulerpartlemgvv  31629  afsval  31937  pthhashvtx  32369  usgrcyclgt2v  32373  cusgr3cyclex  32378  acycgr2v  32392  cusgracyclt3v  32398  mrsubfval  32750  mrsubcv  32752  mrsubff  32754  mrsubrn  32755  elmrsubrn  32762  msubfval  32766  msubff  32772  mpstval  32777  elmpst  32778  msrval  32780  mstaval  32786  msubvrs  32802  mclsssvlem  32804  mclsval  32805  mclsind  32812  mppsval  32814  climlec3  32960  sdclem2  35011  sdclem1  35012  caures  35029  heiborlem3  35085  heibor  35093  grpokerinj  35165  rngoi  35171  dvrunz  35226  isdrngo1  35228  isdrngo2  35230  isrngohom  35237  idlval  35285  isidl  35286  0idl  35297  0rngo  35299  divrngidl  35300  smprngopr  35324  igenval  35333  lshpset  36108  lsatset  36120  lcvfbr  36150  islfl  36190  lfl0f  36199  lfl1  36200  lfladd0l  36204  lflnegl  36206  lflvscl  36207  lflvsdi1  36208  lflvsdi2  36209  lflvsdi2a  36210  lflvsass  36211  lfl0sc  36212  lflsc0N  36213  lfl1sc  36214  lkr0f  36224  lkrsc  36227  eqlkr2  36230  ldualvbase  36256  ldualfvadd  36258  ldualvaddval  36261  ldualsca  36262  ldualfvs  36266  ldualvsval  36268  isopos  36310  cmtfvalN  36340  cvrfval  36398  pats  36415  glbconN  36507  llnset  36635  lplnset  36659  lvolset  36702  lineset  36868  isline  36869  pointsetN  36871  psubspset  36874  ispsubsp  36875  pmapval  36887  paddfval  36927  paddval  36928  pclfvalN  37019  pclvalN  37020  polfvalN  37034  polvalN  37035  psubclsetN  37066  ispsubclN  37067  watvalN  37123  lhpset  37125  lautset  37212  islaut  37213  pautsetN  37228  ispautN  37229  ldilset  37239  ltrnset  37248  dilsetN  37283  cdleme26e  37489  cdleme26eALTN  37491  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdlemefs32sn1aw  37544  cdleme43fsv1snlem  37550  cdleme41sn3a  37563  cdleme32a  37571  cdleme40m  37597  cdleme40n  37598  cdleme42b  37608  tgrpbase  37876  tgrpopr  37877  istendo  37890  tendopl  37906  tendo02  37917  erngbase  37931  erngfplus  37932  erngfmul  37935  erngbase-rN  37939  erngfplus-rN  37940  erngfmul-rN  37943  cdlemk36  38043  cdlemkid  38066  dvasca  38136  dvavbase  38143  dvafvadd  38144  dvafvsca  38146  diafval  38161  diaval  38162  dvhsca  38212  dvhvbase  38217  dvhfvadd  38221  dvhfvsca  38230  docafvalN  38252  docavalN  38253  djafvalN  38264  djavalN  38265  dibfval  38271  dibopelvalN  38273  dibopelval2  38275  dibelval3  38277  diblsmopel  38301  dicfval  38305  dicval  38306  cdlemn11a  38337  dihvalcqpre  38365  dihopelvalcpre  38378  dihord6apre  38386  dihpN  38466  dochfval  38480  dochval  38481  djhfval  38527  djhval  38528  islpolN  38613  lpolconN  38617  dochpolN  38620  lcfrlem9  38680  lcd0vvalN  38743  mapdval  38758  mapd1o  38778  mapdunirnN  38780  mapdhval  38854  mapdhval0  38855  hvmapfval  38889  hvmapval  38890  hdmap1fval  38926  hdmap1vallem  38927  hgmapfval  39016  hlhilset  39064  hlhilbase  39066  hlhilplus  39067  hlhilvsca  39077  hlhilip  39078  hlhilnvl  39080  hlhillsm  39086  hlhillcs  39088  frlmfielbas  39132  islssfgi  39665  pwssplit4  39682  frlmpwfi  39691  mendplusgfval  39778  mendmulrfval  39780  mendvscafval  39783  idomrootle  39788  idomodle  39789  deg1mhm  39800  dvgrat  40637  uzmptshftfval  40671  climexp  41879  climinf  41880  climneg  41884  climdivf  41886  climconstmpt  41932  climresmpt  41933  climsubmpt  41934  fnlimfvre  41948  limsupvaluz  41982  limsupequzmpt2  41992  climuzlem  42017  climisp  42020  climxrrelem  42023  climxrre  42024  limsupgtlem  42051  liminflelimsupuz  42059  liminfgelimsupuz  42062  liminfequzmpt2  42065  liminfvaluz  42066  limsupvaluz3  42072  climliminflimsupd  42075  liminfreuzlem  42076  liminfltlem  42078  liminflimsupclim  42081  liminflbuz2  42089  liminfpnfuz  42090  xlimclim2lem  42113  climxlim2  42120  sge0isum  42703  sge0uzfsumgt  42720  sge0seq  42722  meaiunlelem  42744  caragendifcl  42790  omeiunle  42793  omeiunltfirp  42795  carageniuncl  42799  caragensal  42801  opnssborel  42911  smflimlem6  43046  smfpimcc  43076  smflimmpt  43078  smflimsuplem4  43091  smflimsuplem6  43093  smflimsuplem8  43095  smfliminflem  43098  isomuspgrlem2  43992  ushrisomgr  44000  upwlksfval  44004  isupwlkg  44006  ismgmhm  44044  issubmgm2  44051  submgmacs  44065  copisnmnd  44070  0ringdif  44135  rnghmval  44156  isrnghm  44157  c0snmgmhm  44179  c0snmhm  44180  zrrnghm  44182  zlidlring  44193  cznrng  44220  cznnring  44221  rngchomfvalALTV  44249  rngccofvalALTV  44252  rngccatidALTV  44254  ringchomfvalALTV  44312  ringccofvalALTV  44315  ringccatidALTV  44317  rngcrescrhm  44350  rngcrescrhmALTV  44368  ofaddmndmap  44386  suppmptcfin  44421  mptcfsupp  44422  dmatALTbas  44450  lcoop  44460  linccl  44463  lcosn0  44469  lincvalsc0  44470  lcoc0  44471  linc0scn0  44472  linc1  44474  lincscmcl  44481  islinindfis  44498  lincext1  44503  lincext2  44504  lindslinindimp2lem2  44508  lindslinindimp2lem3  44509  lindsrng01  44517  snlindsntorlem  44519  snlindsntor  44520  ldepspr  44522  lincresunit1  44526  lincresunit2  44527  lines  44712  line  44713  rrxlines  44714  sphere  44728  rrxsphere  44729