Theorem ovexd 7390

Description: The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Assertion

Ref	Expression
ovexd	⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Proof of Theorem ovexd

Step	Hyp	Ref	Expression
1		ovex 7388	. 2 ⊢ (𝐴𝐹𝐵) ∈ V
2	1	a1i 11	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438  (class class class)co 7355

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-sn 4578  df-pr 4580  df-uni 4861  df-iota 6445  df-fv 6497  df-ov 7358

This theorem is referenced by:  caofidlcan  7657  caofass  7659  caofdi  7661  caofdir  7662  caonncan  7663  suppofssd  8142  mapsnend  8968  snmapen  8970  pw2eng  9006  mapen  9064  mapxpen  9066  mapunen  9069  mapdom2  9071  cantnfcl  9567  cantnfle  9571  cantnflt  9572  cantnflt2  9573  cantnfp1lem2  9579  cantnfp1lem3  9580  cantnflem1b  9586  cantnflem1d  9588  cantnflem1  9589  cnfcomlem  9599  cnfcom  9600  cnfcom2lem  9601  cnfcom3lem  9603  fzen  13451  seqf1o  13960  wrdexg  14441  wrdnval  14462  pfxval  14591  pfxswrd  14623  splval  14668  ofccat  14886  climshftlem  15491  climshft  15493  climshft2  15499  caucvgr  15593  fsumrev  15696  hashdvds  16696  setsabs  17100  ressress  17168  firest  17346  prdsvscafval  17394  qusval  17456  xpsbas  17486  xpsadd  17488  xpsmul  17489  xpssca  17490  xpsvsca  17491  xpsless  17492  xpsle  17493  homfval  17608  comfval  17616  cicfval  17714  rescabs  17750  rescabs2  17751  resscat  17769  funcres2c  17820  ressffth  17857  fucbas  17880  fuccoval  17883  setchom  17997  catchom  18020  catcco  18022  estrchom  18043  funcestrcsetclem5  18060  funcsetcestrclem5  18075  evlf2val  18135  curf11  18142  curf12  18143  curf2val  18146  uncfval  18150  diagval  18156  hof2  18173  yonval  18177  resspos  18345  gsumval2a  18603  gsumval2  18604  mndpsuppss  18683  gsumwspan  18764  efmnd  18788  ghmqusnsglem1  19202  ghmqusnsglem2  19203  ghmqusnsg  19204  ghmquskerlem1  19205  ghmquskerco  19206  ghmquskerlem2  19207  ghmquskerlem3  19208  ghmqusker  19209  orbstafun  19233  orbstaval  19234  symgval  19293  psgnvalii  19431  lsmhash  19627  frgpupval  19696  qusabl  19787  gsumval3  19829  gsumreidx  19839  gsumzaddlem  19843  gsummptshft  19858  telgsumfzslem  19910  telgsumfz  19912  telgsumfz0  19914  dpjval  19980  prdsrngd  20104  srgbinomlem3  20156  srgbinomlem4  20157  mulgass3  20281  rngcval  20543  rnghmsscmap2  20554  rnghmsscmap  20555  funcrngcsetc  20565  ringcval  20572  rhmsscmap2  20583  rhmsscmap  20584  funcringcsetc  20599  srhmsubclem3  20604  srhmsubc  20605  fldhmsubc  20710  lcomfsupp  20845  rmodislmodlem  20872  rmodislmod  20873  sraval  21119  srasca  21124  crngridl  21227  quscrng  21230  rhmqusnsg  21232  pzriprnglem11  21438  znval  21482  znzrhfo  21494  znunithash  21511  cygznlem2  21515  frobrhm  21522  pjfval  21653  pjpm  21655  frlmgsum  21719  frlmipval  21726  frlmphllem  21727  frlmphl  21728  frlmsslsp  21743  frlmup1  21745  gsumbagdiaglem  21877  psrass1lem  21879  rhmpsrlem1  21887  psrass1  21911  psrdi  21912  psrdir  21913  psrass23l  21914  psrascl  21926  mplval  21936  mplsubglem  21946  mplsubrglem  21951  mplmonmul  21981  mplcoe1  21982  opsrval  21991  psrbagev1  22022  psrbagev2  22023  evlslem6  22026  evlslem1  22027  evlsval  22031  mpfconst  22046  mpff  22049  mpfaddcl  22050  mpfmulcl  22051  mpfind  22052  mhpmulcl  22074  mhpaddcl  22076  psdcoef  22085  psdmplcl  22087  psdadd  22088  ply1lss  22119  gsumply1subr  22156  coe1add  22188  coe1tm  22197  coe1tmmul  22201  cply1mul  22221  ply1coe  22223  evl1expd  22270  pf1mpf  22277  pf1ind  22280  mhmcompl  22305  mhmcoaddmpl  22306  rhmmpl  22308  rhmply1vsca  22313  mamufv  22319  mamuass  22327  mamuvs1  22330  mamuvs2  22331  matgsum  22362  dmatmul  22422  scmatval  22429  scmatrhmval  22452  mvmulfv  22469  mavmulfv  22471  mavmulass  22474  marrepeval  22488  marepveval  22493  submaeval  22507  mdetrsca  22528  mdetunilem9  22545  mdetuni0  22546  gsummatr01lem3  22582  gsummatr01lem4  22583  gsummatr01  22584  smadiadetlem3  22593  cramerlem1  22612  mat2pmatmul  22656  m2cpminvid  22678  decpmatfsupp  22694  decpmatmullem  22696  decpmatmul  22697  decpmatmulsumfsupp  22698  pmatcollpw1lem1  22699  pmatcollpw3fi1lem1  22711  pmatcollpwscmatlem2  22715  pm2mpfval  22721  pm2mpf  22723  mply1topmatcllem  22728  mp2pm2mplem3  22733  mp2pm2mplem4  22734  pm2mpmhmlem1  22743  pm2mpmhmlem2  22744  pm2mp  22750  chfacfscmulfsupp  22784  chfacfscmulgsum  22785  chfacfpmmulfsupp  22788  chfacfpmmulgsum  22789  cpmidpmatlem3  22797  cpmadugsumlemB  22799  cpmadugsumlemC  22800  cpmadugsumlemF  22801  cayhamlem4  22813  xpstopnlem2  23736  fcfval  23958  tsmsxplem1  24078  tsmsxplem2  24079  tusval  24190  xpsdsfn  24302  xpsxmet  24305  xpsdsval  24306  xpsmet  24307  tmsval  24406  met1stc  24446  metuval  24474  cnmpopc  24859  pi1val  24974  pi1addf  24984  pi1addval  24985  pi1grplem  24986  rrxnm  25328  rrxcph  25329  rrxmval  25342  mbfmulc2  25601  mbfmul  25664  itg2mulclem  25684  ibladd  25759  itgadd  25763  itgabs  25773  bddmulibl  25777  dvmulf  25883  dvcmulf  25885  dvmptmul  25902  cmvth  25932  dvlip  25935  ftc1lem4  25983  mdegmullem  26020  coe1mul3  26041  r1pval  26100  plyco  26183  dgrcolem1  26216  elqaalem3  26266  taylpfval  26309  taylthlem2  26319  taylthlem2OLD  26320  pserdvlem2  26375  advlogexp  26601  logtayl  26606  logccv  26609  dvcxp1  26686  dvcncxp1  26689  logbmpt  26735  logbfval  26737  relogbf  26738  dvatan  26882  cxp2lim  26924  cxploglim2  26926  lgamgulmlem2  26977  lgamgulm2  26983  lgamcvglem  26987  lgamf  26989  basellem7  27034  basellem8  27035  basellem9  27036  fsumdvdscom  27132  logexprlim  27173  dchrfi  27203  gausslemma2dlem2  27315  gausslemma2dlem3  27316  2lgslem1b  27340  chtppilimlem2  27422  chebbnd2  27425  chto1lb  27426  chpchtlim  27427  chpo1ub  27428  vmadivsum  27430  dchrisum0lem3  27467  mudivsum  27478  logdivsum  27481  log2sumbnd  27492  selberglem1  27493  selberg2lem  27498  selberg2  27499  selbergr  27516  negsval  27977  wlkp1  29669  cyclnumvtx  29789  wwlksnextsurj  29889  wwlksnextbij  29891  clwlkclwwlklem2a1  29983  clwlkclwwlkf1  30001  eupth2eucrct  30208  frgrncvvdeq  30300  numclwlk2lem2fv  30369  numclwwlk2lem3  30371  ofoprabco  32657  fsuppcurry1  32718  fsuppcurry2  32719  offinsupp1  32720  ressprs  32958  mntoval  32974  mgcoval  32978  mndlactf1  33018  mndlactfo  33019  mndractf1  33020  mndractfo  33021  mndlactf1o  33022  mndractf1o  33023  lmodvslmhm  33041  gsumwrd2dccat  33058  cycpmco2f1  33104  cycpmco2rn  33105  cycpmco2lem2  33107  cycpmco2lem3  33108  cycpmco2lem4  33109  cycpmco2lem5  33110  cycpmco2lem6  33111  cycpmco2  33113  conjga  33150  cntrval2  33151  fxpsubm  33152  fxpsubg  33153  fxpsubrg  33154  fxpsdrg  33155  archirngz  33169  archiabllem2a  33174  elrgspnlem1  33220  elrgspnlem2  33221  elrgspnsubrunlem2  33226  rlocval  33237  fracval  33281  quslmod  33334  quslmhm  33335  quslvec  33336  qustriv  33340  qustrivr  33341  unitprodclb  33365  nsgmgc  33388  nsgqusf1olem1  33389  nsgqusf1olem2  33390  nsgqusf1olem3  33391  lmhmqusker  33393  rhmquskerlem  33401  elrspunidl  33404  qsidomlem1  33428  qsidomlem2  33429  opprqusbas  33464  opprqusplusg  33465  opprqusmulr  33467  opprqus1r  33468  qsdrngilem  33470  qsdrngi  33471  rprmdvdsprod  33510  1arithidomlem1  33511  1arithidomlem2  33512  1arithidom  33513  1arithufdlem3  33522  dfufd2lem  33525  zringfrac  33530  evl1deg1  33550  evl1deg2  33551  evl1deg3  33552  ply1gsumz  33570  r1plmhm  33581  mplvrpmrhm  33588  splyval  33593  resssra  33610  ply1degltdimlem  33646  ply1degltdim  33647  qusdimsum  33652  fedgmullem1  33653  fedgmullem2  33654  fedgmul  33655  lactlmhm  33658  fldgenfldext  33692  evls1fldgencl  33694  fldextrspunlsplem  33697  fldextrspundgdvdslem  33704  fldextrspundgdvds  33705  extdgfialglem1  33716  extdgfialglem2  33717  extdgfialg  33718  algextdeglem4  33744  algextdeglem6  33746  algextdeglem7  33747  submateq  33833  lmatcl  33840  mdetpmtr1  33847  madjusmdetlem1  33851  madjusmdetlem3  33853  qqhvval  34007  esumfzf  34093  esumpfinvallem  34098  esumpmono  34103  esummulc1  34105  esumcvg  34110  esumgect  34114  ofcval  34123  omssubadd  34324  sitgfval  34365  sitmcl  34375  sseqfv2  34418  cndprobval  34457  ballotlemfval  34514  ballotlemsv  34534  ballotlemsf1o  34538  ofcccat  34567  signsplypnf  34574  signsply0  34575  signstfval  34588  signshf  34612  reprpmtf1o  34650  reprdifc  34651  logdivsqrle  34674  hgt750lemg  34678  hgt750lema  34681  lpadval  34700  cvmliftlem8  35347  cvmliftphtlem  35372  fmla1  35442  gonarlem  35449  sategoelfvb  35474  mrsubval  35564  ellcsrspsn  35696  r1peuqusdeg1  35698  fwddifval  36217  knoppcnlem1  36548  knoppcnlem6  36553  unbdqndv2lem2  36565  poimirlem1  37671  poimirlem2  37672  poimirlem3  37673  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem16  37686  poimirlem19  37689  poimirlem22  37692  poimirlem23  37693  broucube  37704  dvtan  37720  itg2addnc  37724  ibladdnc  37727  itgaddnc  37730  itgmulc2nclem2  37737  itgmulc2nc  37738  itgabsnc  37739  ftc1cnnclem  37741  ftc1anclem3  37745  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  dvasin  37754  dvacos  37755  dvreasin  37756  dvreacos  37757  areacirclem1  37758  areacirc  37763  fsumshftd  39061  hlrelat5N  39510  rhmzrhval  42074  aks6d1c1  42219  hashscontpow  42225  aks6d1c4  42227  aks6d1c2lem3  42229  aks6d1c2lem4  42230  aks6d1c2  42233  aks6d1c5lem0  42238  aks6d1c5lem3  42240  aks6d1c5lem2  42241  aks6d1c5  42242  sticksstones3  42251  sticksstones8  42256  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  aks6d1c6lem1  42273  aks6d1c6lem2  42274  aks6d1c6lem3  42275  aks6d1c6lem4  42276  aks6d1c6isolem1  42277  aks6d1c6isolem2  42278  aks6d1c6isolem3  42279  aks6d1c6lem5  42280  aks6d1c7lem2  42284  unitscyglem1  42298  readvrec2  42469  readvrec  42470  readvcot  42472  frlmfzolen  42611  frlmfzoccat  42613  frlmvscadiccat  42614  evlscl  42666  evlsval3  42667  evlsvval  42668  evlsvvval  42671  evlsbagval  42674  evlsexpval  42675  evlsaddval  42676  evlsmulval  42677  evlsevl  42679  evlcl  42680  evladdval  42683  evlmulval  42684  selvcl  42691  evlselv  42695  fsuppind  42698  mhpind  42702  mhphflem  42704  prjspner  42727  prjspnvs  42728  prjspnfv01  42732  prjspner01  42733  prjspner1  42734  0prjspnrel  42735  prjcrv0  42741  mzpclall  42834  mzpsubst  42855  eldioph2  42869  rabdiophlem2  42909  irrapxlem1  42929  mzpcong  43079  mendlmod  43296  naddcnff  43469  relexpmulnn  43816  iunrelexpuztr  43826  mnringvald  44320  mnringmulrvald  44334  radcnvrat  44421  hashnzfzclim  44429  lhe4.4ex1a  44436  expgrowthi  44440  expgrowth  44442  bccval  44445  binomcxplemrat  44457  binomcxplemfrat  44458  binomcxplemradcnv  44459  binomcxplemdvbinom  44460  binomcxplemdvsum  44462  binomcxplemnotnn0  44463  unirnmap  45319  unirnmapsn  45325  ssmapsn  45327  iocopn  45634  icoopn  45639  divcnvg  45741  sumnnodd  45744  climsubmpt  45772  dvsinax  46025  fperdvper  46031  dvdivf  46034  dvnprodlem1  46058  itgsincmulx  46086  stoweidlem59  46171  etransclem4  46350  etransclem13  46359  etransclem25  46371  etransclem48  46394  rrxtopnfi  46399  sge0tsms  46492  elhoi  46654  ovnval2  46657  ovnval2b  46664  ovncvrrp  46676  ovn0lem  46677  ovncl  46679  ovnome  46685  hoidmvlelem2  46708  hoidmvlelem3  46709  hoidmvle  46712  ovnlecvr2  46722  ovncvr2  46723  ovnsubadd2lem  46757  ovnovollem1  46768  vonvolmbl  46773  iunhoiioolem  46787  vonioolem1  46792  vonioolem2  46793  vonicclem2  46796  smfresal  46900  smfres  46902  smfmullem4  46906  smfco  46914  adddmmbl  46945  muldmmbl  46947  chnsuslle  46993  nthrucw  46998  sinnpoly  47005  fmtno  47643  isubgruhgr  47982  grtriprop  48055  grtriclwlk3  48059  gpgvtx  48157  gpgiedg  48158  intopval  48316  clintopval  48318  rngchomALTV  48382  funcringcsetcALTV2lem5  48408  ringchomALTV  48416  funcringcsetclem5ALTV  48431  srhmsubcALTVlem2  48438  srhmsubcALTV  48439  fldhmsubcALTV  48447  zlmodzxzscm  48471  zlmodzxzadd  48472  rmsupp0  48482  domnmsuppn0  48483  rmsuppss  48484  ply1mulgsumlem3  48503  ply1mulgsumlem4  48504  ply1mulgsum  48505  dmatALTval  48515  lincop  48523  lincval  48524  linc1  48540  lincresunit3lem1  48594  fdivmpt  48655  fdivmptfv  48660  refdivmptfv  48661  digval  48713  2arymptfv  48765  2arymaptfo  48769  itcovalpclem1  48785  itcovalt2lem1  48790  ackvalsuc1mpt  48793  ackval1  48796  ackval2  48797  ackval3  48798  ackval42  48811  line2xlem  48868  upfval2  49292  swapfval  49377  tposcurf1  49414  tposcurf2val  49416  fucofvalg  49433  fuco112x  49447  fuco23  49456  fucoid  49463  fucocolem4  49471  prcofvalg  49491  prcof1  49503  opf2fval  49520  lanval  49734  ranval  49735