Theorem ovexd 7405

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 7403	. 2 ⊢ (𝐴𝐹𝐵) ∈ V
2	1	a1i 11	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  (class class class)co 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5255

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  caofidlcan  7672  caofass  7674  caofdi  7676  caofdir  7677  caonncan  7678  suppofssd  8157  mapsnend  8987  snmapen  8989  pw2eng  9025  mapen  9083  mapxpen  9085  mapunen  9088  mapdom2  9090  cantnfcl  9590  cantnfle  9594  cantnflt  9595  cantnflt2  9596  cantnfp1lem2  9602  cantnfp1lem3  9603  cantnflem1b  9609  cantnflem1d  9611  cantnflem1  9612  cnfcomlem  9622  cnfcom  9623  cnfcom2lem  9624  cnfcom3lem  9626  fzen  13471  seqf1o  13980  wrdexg  14461  wrdnval  14482  pfxval  14611  pfxswrd  14643  splval  14688  ofccat  14906  climshftlem  15511  climshft  15513  climshft2  15519  caucvgr  15613  fsumrev  15716  hashdvds  16716  setsabs  17120  ressress  17188  firest  17366  prdsvscafval  17414  qusval  17477  xpsbas  17507  xpsadd  17509  xpsmul  17510  xpssca  17511  xpsvsca  17512  xpsless  17513  xpsle  17514  homfval  17629  comfval  17637  cicfval  17735  rescabs  17771  rescabs2  17772  resscat  17790  funcres2c  17841  ressffth  17878  fucbas  17901  fuccoval  17904  setchom  18018  catchom  18041  catcco  18043  estrchom  18064  funcestrcsetclem5  18081  funcsetcestrclem5  18096  evlf2val  18156  curf11  18163  curf12  18164  curf2val  18167  uncfval  18171  diagval  18177  hof2  18194  yonval  18198  resspos  18366  gsumval2a  18624  gsumval2  18625  mndpsuppss  18704  gsumwspan  18785  efmnd  18809  ghmqusnsglem1  19226  ghmqusnsglem2  19227  ghmqusnsg  19228  ghmquskerlem1  19229  ghmquskerco  19230  ghmquskerlem2  19231  ghmquskerlem3  19232  ghmqusker  19233  orbstafun  19257  orbstaval  19258  symgval  19317  psgnvalii  19455  lsmhash  19651  frgpupval  19720  qusabl  19811  gsumval3  19853  gsumreidx  19863  gsumzaddlem  19867  gsummptshft  19882  telgsumfzslem  19934  telgsumfz  19936  telgsumfz0  19938  dpjval  20004  prdsrngd  20128  srgbinomlem3  20180  srgbinomlem4  20181  mulgass3  20306  rngcval  20568  rnghmsscmap2  20579  rnghmsscmap  20580  funcrngcsetc  20590  ringcval  20597  rhmsscmap2  20608  rhmsscmap  20609  funcringcsetc  20624  srhmsubclem3  20629  srhmsubc  20630  fldhmsubc  20735  lcomfsupp  20870  rmodislmodlem  20897  rmodislmod  20898  sraval  21144  srasca  21149  crngridl  21252  quscrng  21255  rhmqusnsg  21257  pzriprnglem11  21463  znval  21507  znzrhfo  21519  znunithash  21536  cygznlem2  21540  frobrhm  21547  pjfval  21678  pjpm  21680  frlmgsum  21744  frlmipval  21751  frlmphllem  21752  frlmphl  21753  frlmsslsp  21768  frlmup1  21770  gsumbagdiaglem  21903  psrass1lem  21905  rhmpsrlem1  21913  psrass1  21936  psrdi  21937  psrdir  21938  psrass23l  21939  psrascl  21951  mplval  21961  mplsubglem  21971  mplsubrglem  21976  mplmonmul  22008  mplcoe1  22009  opsrval  22018  psrbagev1  22049  psrbagev2  22050  evlslem6  22053  evlslem1  22054  evlsval  22058  evlsval3  22061  evlsvval  22062  evlsvvval  22065  evlcl  22074  evladdval  22075  evlmulval  22076  mpfconst  22081  mpff  22084  mpfaddcl  22085  mpfmulcl  22086  mpfind  22087  mhpmulcl  22109  mhpaddcl  22111  psdcoef  22120  psdmplcl  22122  psdadd  22123  ply1lss  22154  gsumply1subr  22191  coe1add  22223  coe1tm  22232  coe1tmmul  22236  cply1mul  22257  ply1coe  22259  evl1expd  22306  pf1mpf  22313  pf1ind  22316  mhmcompl  22341  mhmcoaddmpl  22342  rhmmpl  22344  rhmply1vsca  22349  mamufv  22355  mamuass  22363  mamuvs1  22366  mamuvs2  22367  matgsum  22398  dmatmul  22458  scmatval  22465  scmatrhmval  22488  mvmulfv  22505  mavmulfv  22507  mavmulass  22510  marrepeval  22524  marepveval  22529  submaeval  22543  mdetrsca  22564  mdetunilem9  22581  mdetuni0  22582  gsummatr01lem3  22618  gsummatr01lem4  22619  gsummatr01  22620  smadiadetlem3  22629  cramerlem1  22648  mat2pmatmul  22692  m2cpminvid  22714  decpmatfsupp  22730  decpmatmullem  22732  decpmatmul  22733  decpmatmulsumfsupp  22734  pmatcollpw1lem1  22735  pmatcollpw3fi1lem1  22747  pmatcollpwscmatlem2  22751  pm2mpfval  22757  pm2mpf  22759  mply1topmatcllem  22764  mp2pm2mplem3  22769  mp2pm2mplem4  22770  pm2mpmhmlem1  22779  pm2mpmhmlem2  22780  pm2mp  22786  chfacfscmulfsupp  22820  chfacfscmulgsum  22821  chfacfpmmulfsupp  22824  chfacfpmmulgsum  22825  cpmidpmatlem3  22833  cpmadugsumlemB  22835  cpmadugsumlemC  22836  cpmadugsumlemF  22837  cayhamlem4  22849  xpstopnlem2  23772  fcfval  23994  tsmsxplem1  24114  tsmsxplem2  24115  tusval  24226  xpsdsfn  24338  xpsxmet  24341  xpsdsval  24342  xpsmet  24343  tmsval  24442  met1stc  24482  metuval  24510  cnmpopc  24895  pi1val  25010  pi1addf  25020  pi1addval  25021  pi1grplem  25022  rrxnm  25364  rrxcph  25365  rrxmval  25378  mbfmulc2  25637  mbfmul  25700  itg2mulclem  25720  ibladd  25795  itgadd  25799  itgabs  25809  bddmulibl  25813  dvmulf  25919  dvcmulf  25921  dvmptmul  25938  cmvth  25968  dvlip  25971  ftc1lem4  26019  mdegmullem  26056  coe1mul3  26077  r1pval  26136  plyco  26219  dgrcolem1  26252  elqaalem3  26302  taylpfval  26345  taylthlem2  26355  taylthlem2OLD  26356  pserdvlem2  26411  advlogexp  26637  logtayl  26642  logccv  26645  dvcxp1  26722  dvcncxp1  26725  logbmpt  26771  logbfval  26773  relogbf  26774  dvatan  26918  cxp2lim  26960  cxploglim2  26962  lgamgulmlem2  27013  lgamgulm2  27019  lgamcvglem  27023  lgamf  27025  basellem7  27070  basellem8  27071  basellem9  27072  fsumdvdscom  27168  logexprlim  27209  dchrfi  27239  gausslemma2dlem2  27351  gausslemma2dlem3  27352  2lgslem1b  27376  chtppilimlem2  27458  chebbnd2  27461  chto1lb  27462  chpchtlim  27463  chpo1ub  27464  vmadivsum  27466  dchrisum0lem3  27503  mudivsum  27514  logdivsum  27517  log2sumbnd  27528  selberglem1  27529  selberg2lem  27534  selberg2  27535  selbergr  27552  negsval  28038  wlkp1  29771  cyclnumvtx  29891  wwlksnextsurj  29991  wwlksnextbij  29993  clwlkclwwlklem2a1  30085  clwlkclwwlkf1  30103  eupth2eucrct  30310  frgrncvvdeq  30402  numclwlk2lem2fv  30471  numclwwlk2lem3  30473  ofoprabco  32760  fsuppcurry1  32820  fsuppcurry2  32821  offinsupp1  32822  ressprs  33065  mntoval  33081  mgcoval  33085  mndlactf1  33125  mndlactfo  33126  mndractf1  33127  mndractfo  33128  mndlactf1o  33129  mndractf1o  33130  lmodvslmhm  33150  gsummulsubdishift2  33169  gsumwrd2dccat  33178  cycpmco2f1  33224  cycpmco2rn  33225  cycpmco2lem2  33227  cycpmco2lem3  33228  cycpmco2lem4  33229  cycpmco2lem5  33230  cycpmco2lem6  33231  cycpmco2  33233  conjga  33270  cntrval2  33271  fxpsubm  33272  fxpsubg  33273  fxpsubrg  33274  fxpsdrg  33275  archirngz  33289  archiabllem2a  33294  elrgspnlem1  33342  elrgspnlem2  33343  elrgspnsubrunlem2  33348  rlocval  33359  fracval  33404  quslmod  33457  quslmhm  33458  quslvec  33459  qustriv  33463  qustrivr  33464  unitprodclb  33488  nsgmgc  33511  nsgqusf1olem1  33512  nsgqusf1olem2  33513  nsgqusf1olem3  33514  lmhmqusker  33516  rhmquskerlem  33524  elrspunidl  33527  qsidomlem1  33551  qsidomlem2  33552  opprqusbas  33587  opprqusplusg  33588  opprqusmulr  33590  opprqus1r  33591  qsdrngilem  33593  qsdrngi  33594  rprmdvdsprod  33633  1arithidomlem1  33634  1arithidomlem2  33635  1arithidom  33636  1arithufdlem3  33645  dfufd2lem  33648  zringfrac  33653  evl1deg1  33675  evl1deg2  33676  evl1deg3  33677  ply1gsumz  33698  r1plmhm  33709  mplvrpmrhm  33730  psrgsum  33731  psrmonmul  33733  psrmonprod  33735  mplgsum  33736  splyval  33742  esplyfval1  33756  esplyfvaln  33757  vietadeg1  33761  resssra  33770  ply1degltdimlem  33806  ply1degltdim  33807  qusdimsum  33812  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  lactlmhm  33818  fldgenfldext  33852  evls1fldgencl  33854  fldextrspunlsplem  33857  fldextrspundgdvdslem  33864  fldextrspundgdvds  33865  extdgfialglem1  33876  extdgfialglem2  33877  extdgfialg  33878  algextdeglem4  33904  algextdeglem6  33906  algextdeglem7  33907  submateq  33993  lmatcl  34000  mdetpmtr1  34007  madjusmdetlem1  34011  madjusmdetlem3  34013  qqhvval  34167  esumfzf  34253  esumpfinvallem  34258  esumpmono  34263  esummulc1  34265  esumcvg  34270  esumgect  34274  ofcval  34283  omssubadd  34484  sitgfval  34525  sitmcl  34535  sseqfv2  34578  cndprobval  34617  ballotlemfval  34674  ballotlemsv  34694  ballotlemsf1o  34698  ofcccat  34727  signsplypnf  34734  signsply0  34735  signstfval  34748  signshf  34772  reprpmtf1o  34810  reprdifc  34811  logdivsqrle  34834  hgt750lemg  34838  hgt750lema  34841  lpadval  34860  cvmliftlem8  35514  cvmliftphtlem  35539  fmla1  35609  gonarlem  35616  sategoelfvb  35641  mrsubval  35731  ellcsrspsn  35863  r1peuqusdeg1  35865  fwddifval  36384  knoppcnlem1  36721  knoppcnlem6  36726  unbdqndv2lem2  36738  poimirlem1  37901  poimirlem2  37902  poimirlem3  37903  poimirlem5  37905  poimirlem6  37906  poimirlem7  37907  poimirlem10  37910  poimirlem11  37911  poimirlem12  37912  poimirlem16  37916  poimirlem19  37919  poimirlem22  37922  poimirlem23  37923  broucube  37934  dvtan  37950  itg2addnc  37954  ibladdnc  37957  itgaddnc  37960  itgmulc2nclem2  37967  itgmulc2nc  37968  itgabsnc  37969  ftc1cnnclem  37971  ftc1anclem3  37975  ftc1anclem6  37978  ftc1anclem7  37979  ftc1anclem8  37980  dvasin  37984  dvacos  37985  dvreasin  37986  dvreacos  37987  areacirclem1  37988  areacirc  37993  fsumshftd  39357  hlrelat5N  39806  rhmzrhval  42370  aks6d1c1  42515  hashscontpow  42521  aks6d1c4  42523  aks6d1c2lem3  42525  aks6d1c2lem4  42526  aks6d1c2  42529  aks6d1c5lem0  42534  aks6d1c5lem3  42536  aks6d1c5lem2  42537  aks6d1c5  42538  sticksstones3  42547  sticksstones8  42552  sticksstones10  42554  sticksstones12a  42556  sticksstones12  42557  aks6d1c6lem1  42569  aks6d1c6lem2  42570  aks6d1c6lem3  42571  aks6d1c6lem4  42572  aks6d1c6isolem1  42573  aks6d1c6isolem2  42574  aks6d1c6isolem3  42575  aks6d1c6lem5  42576  aks6d1c7lem2  42580  unitscyglem1  42594  readvrec2  42760  readvrec  42761  readvcot  42763  frlmfzolen  42902  frlmfzoccat  42904  frlmvscadiccat  42905  evlscl  42953  evlsbagval  42956  evlsexpval  42957  evlsaddval  42958  evlsmulval  42959  evlsevl  42961  selvcl  42970  evlselv  42974  fsuppind  42977  mhpind  42981  mhphflem  42983  prjspner  43006  prjspnvs  43007  prjspnfv01  43011  prjspner01  43012  prjspner1  43013  0prjspnrel  43014  prjcrv0  43020  mzpclall  43113  mzpsubst  43134  eldioph2  43148  rabdiophlem2  43188  irrapxlem1  43208  mzpcong  43358  mendlmod  43575  naddcnff  43748  relexpmulnn  44094  iunrelexpuztr  44104  mnringvald  44598  mnringmulrvald  44612  radcnvrat  44699  hashnzfzclim  44707  lhe4.4ex1a  44714  expgrowthi  44718  expgrowth  44720  bccval  44723  binomcxplemrat  44735  binomcxplemfrat  44736  binomcxplemradcnv  44737  binomcxplemdvbinom  44738  binomcxplemdvsum  44740  binomcxplemnotnn0  44741  unirnmap  45595  unirnmapsn  45601  ssmapsn  45603  iocopn  45909  icoopn  45914  divcnvg  46016  sumnnodd  46019  climsubmpt  46047  dvsinax  46300  fperdvper  46306  dvdivf  46309  dvnprodlem1  46333  itgsincmulx  46361  stoweidlem59  46446  etransclem4  46625  etransclem13  46634  etransclem25  46646  etransclem48  46669  rrxtopnfi  46674  sge0tsms  46767  elhoi  46929  ovnval2  46932  ovnval2b  46939  ovncvrrp  46951  ovn0lem  46952  ovncl  46954  ovnome  46960  hoidmvlelem2  46983  hoidmvlelem3  46984  hoidmvle  46987  ovnlecvr2  46997  ovncvr2  46998  ovnsubadd2lem  47032  ovnovollem1  47043  vonvolmbl  47048  iunhoiioolem  47062  vonioolem1  47067  vonioolem2  47068  vonicclem2  47071  smfresal  47175  smfres  47177  smfmullem4  47181  smfco  47189  adddmmbl  47220  muldmmbl  47222  chnsuslle  47268  nthrucw  47273  sinnpoly  47280  fmtno  47918  isubgruhgr  48257  grtriprop  48330  grtriclwlk3  48334  gpgvtx  48432  gpgiedg  48433  intopval  48591  clintopval  48593  rngchomALTV  48657  funcringcsetcALTV2lem5  48683  ringchomALTV  48691  funcringcsetclem5ALTV  48706  srhmsubcALTVlem2  48713  srhmsubcALTV  48714  fldhmsubcALTV  48722  zlmodzxzscm  48746  zlmodzxzadd  48747  rmsupp0  48757  domnmsuppn0  48758  rmsuppss  48759  ply1mulgsumlem3  48777  ply1mulgsumlem4  48778  ply1mulgsum  48779  dmatALTval  48789  lincop  48797  lincval  48798  linc1  48814  lincresunit3lem1  48868  fdivmpt  48929  fdivmptfv  48934  refdivmptfv  48935  digval  48987  2arymptfv  49039  2arymaptfo  49043  itcovalpclem1  49059  itcovalt2lem1  49064  ackvalsuc1mpt  49067  ackval1  49070  ackval2  49071  ackval3  49072  ackval42  49085  line2xlem  49142  upfval2  49565  swapfval  49650  tposcurf1  49687  tposcurf2val  49689  fucofvalg  49706  fuco112x  49720  fuco23  49729  fucoid  49736  fucocolem4  49744  prcofvalg  49764  prcof1  49776  opf2fval  49793  lanval  50007  ranval  50008