Theorem ovexd 7455

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4584  df-pr 4586  df-uni 4867  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  caofidlcan  7731  caofass  7733  caofdi  7735  caofdir  7736  caonncan  7737  suppofssd  8220  mapsnend  9064  snmapen  9066  pw2eng  9102  mapen  9160  mapxpen  9162  mapunen  9165  mapdom2  9167  cantnfcl  9668  cantnfle  9672  cantnflt  9673  cantnflt2  9674  cantnfp1lem2  9680  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1d  9689  cantnflem1  9690  cnfcomlem  9700  cnfcom  9701  cnfcom2lem  9702  cnfcom3lem  9704  fzen  13674  seqf1o  14186  wrdexg  14669  wrdnval  14690  pfxval  14823  pfxswrd  14855  splval  14900  s3rex  15101  s3rexrd  15102  ofccat  15122  climshftlem  15741  climshft  15743  climshft2  15749  caucvgr  15843  fsumrev  15945  hashdvds  16952  setsabs  17357  ressress  17425  firest  17603  prdsvscafval  17651  qusval  17714  xpsbas  17744  xpsadd  17746  xpsmul  17747  xpssca  17748  xpsvsca  17749  xpsless  17750  xpsle  17751  homfval  17866  comfval  17874  cicfval  17972  rescabs  18008  rescabs2  18009  resscat  18027  funcres2c  18078  ressffth  18115  fucbas  18138  fuccoval  18141  setchom  18255  catchom  18278  catcco  18280  estrchom  18301  funcestrcsetclem5  18318  funcsetcestrclem5  18333  evlf2val  18393  curf11  18400  curf12  18401  curf2val  18404  uncfval  18408  diagval  18414  hof2  18431  yonval  18435  resspos  18603  gsumval2a  18874  gsumval2  18875  mndpsuppss  18959  gsumwspan  19042  efmnd  19066  qustriv  19396  qustrivr  19397  ghmqusnsglem1  19494  ghmqusnsglem2  19495  ghmqusnsg  19496  ghmquskerlem1  19497  ghmquskerco  19498  ghmquskerlem2  19499  ghmquskerlem3  19500  ghmqusker  19501  orbstafun  19525  orbstaval  19526  symgval  19585  psgnvalii  19723  lsmhash  19919  frgpupval  19988  qusabl  20079  gsumval3  20121  gsumreidx  20131  gsumzaddlem  20135  gsummptshft  20150  telgsumfzslem  20202  telgsumfz  20204  telgsumfz0  20206  dpjval  20272  prdsrngd  20398  srgbinomlem3  20454  srgbinomlem4  20455  mulgass3  20583  rngcval  20870  rnghmsscmap2  20881  rnghmsscmap  20882  funcrngcsetc  20892  ringcval  20899  rhmsscmap2  20910  rhmsscmap  20911  funcringcsetc  20926  srhmsubclem3  20931  srhmsubc  20932  fldhmsubc  21042  lcomfsupp  21177  rmodislmodlem  21204  rmodislmod  21205  sraval  21450  srasca  21455  crngridl  21575  quscrng  21579  rhmqusnsg  21581  qsidomlem1  21636  qsidomlem2  21637  pzriprnglem11  21797  znval  21841  znzrhfo  21853  znunithash  21870  cygznlem2  21874  frobrhm  21881  pjfval  22012  pjpm  22014  frlmgsum  22078  frlmipval  22085  frlmphllem  22086  frlmphl  22087  frlmsslsp  22102  frlmup1  22104  gsumbagdiaglem  22239  psrass1lem  22241  rhmpsrlem1  22248  psrass1  22271  psrdi  22272  psrdir  22273  psrass23l  22274  psrascl  22286  mplval  22296  mplsubglem  22306  mplsubrglem  22311  mplmonmul  22345  mplcoe1  22346  opsrval  22355  psrbagev1  22386  psrbagev2  22387  evlslem6  22390  evlslem1  22391  evlsval  22395  evlsval3  22398  evlsvval  22399  evlsvvval  22402  evlcl  22411  evladdval  22412  evlmulval  22413  mpfconst  22418  mpff  22421  mpfaddcl  22422  mpfmulcl  22423  mpfind  22424  mhmcompl  22430  mhmcoaddmpl  22432  evlscl  22434  evlsexpval  22437  evlsaddval  22438  evlsmulval  22439  evlsevl  22441  selvcl  22449  mhpmulcl  22470  mhpaddcl  22472  psdcoef  22481  psdmplcl  22483  psdadd  22484  ply1lss  22514  gsumply1subr  22551  coe1add  22583  coe1tm  22592  coe1tmmul  22596  cply1mul  22614  ply1coe  22616  evl1expd  22663  pf1mpf  22670  pf1ind  22673  rhmmpl  22698  rhmply1vsca  22703  mamufv  22709  mamuass  22717  mamuvs1  22720  mamuvs2  22721  matgsum  22752  dmatmul  22812  scmatval  22819  scmatrhmval  22842  mvmulfv  22859  mavmulfv  22861  mavmulass  22864  marrepeval  22878  marepveval  22883  submaeval  22897  mdetrsca  22918  mdetunilem9  22935  mdetuni0  22936  gsummatr01lem3  22972  gsummatr01lem4  22973  gsummatr01  22974  smadiadetlem3  22983  cramerlem1  23005  mat2pmatmul  23049  m2cpminvid  23071  decpmatfsupp  23087  decpmatmullem  23089  decpmatmul  23090  decpmatmulsumfsupp  23091  pmatcollpw1lem1  23092  pmatcollpw3fi1lem1  23104  pmatcollpwscmatlem2  23108  pm2mpfval  23114  pm2mpf  23116  mply1topmatcllem  23121  mp2pm2mplem3  23126  mp2pm2mplem4  23127  pm2mpmhmlem1  23136  pm2mpmhmlem2  23137  pm2mp  23143  chfacfscmulfsupp  23177  chfacfscmulgsum  23178  chfacfpmmulfsupp  23181  chfacfpmmulgsum  23182  cpmidpmatlem3  23190  cpmadugsumlemB  23192  cpmadugsumlemC  23193  cpmadugsumlemF  23194  cayhamlem4  23206  xpstopnlem2  24130  fcfval  24352  tsmsxplem1  24472  tsmsxplem2  24473  tusval  24584  xpsdsfn  24696  xpsxmet  24699  xpsdsval  24700  xpsmet  24701  tmsval  24800  met1stc  24840  metuval  24868  cnmpopc  25249  pi1val  25358  pi1addf  25368  pi1addval  25369  pi1grplem  25370  rrxnm  25712  rrxcph  25713  rrxmval  25726  mbfmulc2  25984  mbfmul  26047  itg2mulclem  26067  ibladd  26141  itgadd  26145  itgabs  26155  bddmulibl  26159  dvmulf  26263  dvcmulf  26265  dvmptmul  26281  cmvth  26311  dvlip  26313  ftc1lem4  26359  mdegmullem  26396  coe1mul3  26417  r1pval  26476  plyco  26560  dgrcolem1  26592  elqaalem3  26644  taylpfval  26692  taylthlem2  26701  pserdvlem2  26755  advlogexp  26983  logtayl  26988  logccv  26991  dvcxp1  27068  dvcncxp1  27071  logbmpt  27116  logbfval  27118  relogbf  27119  dvatan  27263  cxp2lim  27304  cxploglim2  27306  lgamgulmlem2  27357  lgamgulm2  27363  lgamcvglem  27367  lgamf  27369  basellem7  27414  basellem8  27415  basellem9  27416  fsumdvdscom  27512  logexprlim  27552  dchrfi  27582  gausslemma2dlem2  27694  gausslemma2dlem3  27695  2lgslem1b  27719  chtppilimlem2  27801  chebbnd2  27804  chto1lb  27805  chpchtlim  27806  chpo1ub  27807  vmadivsum  27809  dchrisum0lem3  27846  mudivsum  27857  logdivsum  27860  log2sumbnd  27871  selberglem1  27872  selberg2lem  27877  selberg2  27878  selbergr  27895  negsval  28411  cgrabasimass  29378  angmgmval  29394  wlkp1  30260  cyclnumvtx  30388  wwlksnextsurj  30489  wwlksnextbij  30491  clwlkclwwlklem2a1  30583  clwlkclwwlkf1  30601  eupth2eucrct  30818  frgrncvvdeq  30910  numclwlk2lem2fv  30979  numclwwlk2lem3  30981  ofoprabco  33300  fsuppcurry1  33358  fsuppcurry2  33359  offinsupp1  33360  ressprs  33569  mntoval  33585  mgcoval  33589  mndlactf1  33629  mndlactfo  33630  mndractf1  33631  mndractfo  33632  mndlactf1o  33633  mndractf1o  33634  lmodvslmhm  33653  gsummulsubdishift2  33672  gsumwrd2dccat  33681  cycpmco2f1  33727  cycpmco2rn  33728  cycpmco2lem2  33730  cycpmco2lem3  33731  cycpmco2lem4  33732  cycpmco2lem5  33733  cycpmco2lem6  33734  cycpmco2  33736  conjga  33773  cntrval2  33774  fxpsubm  33775  fxpsubg  33776  fxpsubrg  33777  fxpsdrg  33778  archirngz  33792  archiabllem2a  33797  elrgspnlem1  33845  elrgspnlem2  33846  elrgspnsubrunlem2  33851  rlocval  33862  fracval  33908  quslmod  33961  quslmhm  33962  quslvec  33963  unitprodclb  33986  nsgmgc  34005  nsgqusf1olem1  34006  nsgqusf1olem2  34007  nsgqusf1olem3  34008  lmhmqusker  34010  rhmquskerlem  34017  elrspunidl  34020  opprqusbas  34054  opprqusplusg  34055  opprqusmulr  34057  opprqus1r  34058  qsdrngilem  34060  qsdrngi  34061  rprmdvdsprod  34108  1arithidomlem1  34109  1arithidomlem2  34110  1arithidom  34111  1arithufdlem3  34120  dfufd2lem  34123  zringfrac  34128  evl1deg1  34150  evl1deg2  34151  evl1deg3  34152  ply1gsumz  34173  r1plmhm  34183  0mplrim  34188  selvply1rhmlema  34192  selvply1rhmlemb  34193  selvply1rhmlem1  34194  selvply1rhmlem3  34196  selvply1rhmlem4  34197  selvply1rhmlem5  34198  mplvrpmrhm  34221  psrgsum  34222  psrmonmul  34224  psrmonprod  34226  mplgsum  34227  splyval  34233  esplyfval1  34247  esplyfvaln  34248  vietadeg1  34252  resssra  34261  ply1degltdimlem  34296  ply1degltdim  34297  qusdimsum  34302  fedgmullem1  34303  fedgmullem2  34304  fedgmul  34305  lactlmhm  34308  fldgenfldext  34342  evls1fldgencl  34344  fldextrspunlsplem  34347  fldextrspundgdvdslem  34354  fldextrspundgdvds  34355  extdgfialglem1  34366  extdgfialglem2  34367  algextdeglem4  34394  algextdeglem6  34396  algextdeglem7  34397  submateq  34483  lmatcl  34490  mdetpmtr1  34497  madjusmdetlem1  34501  madjusmdetlem3  34503  qqhvval  34657  esumfzf  34743  esumpfinvallem  34748  esumpmono  34753  esummulc1  34755  esumcvg  34760  esumgect  34764  ofcval  34773  omssubadd  34974  sitgfval  35015  sitmcl  35025  sseqfv2  35068  cndprobval  35107  ballotlemfval  35164  ballotlemsv  35184  ballotlemsf1o  35188  ofcccat  35217  signsplypnf  35221  signsply0  35222  signstfval  35235  signshf  35259  reprpmtf1o  35297  reprdifc  35298  logdivsqrle  35321  hgt750lemg  35325  hgt750lema  35328  lpadval  35350  cvmliftlem8  36099  cvmliftphtlem  36124  fmla1  36194  gonarlem  36201  sategoelfvb  36226  mrsubval  36316  ellcsrspsn  36448  r1peuqusdeg1  36450  fwddifval  36969  knoppcnlem1  37401  knoppcnlem6  37406  unbdqndv2lem2  37418  poimirlem1  38582  poimirlem2  38583  poimirlem3  38584  poimirlem5  38586  poimirlem6  38587  poimirlem7  38588  poimirlem10  38591  poimirlem11  38592  poimirlem12  38593  poimirlem16  38597  poimirlem19  38600  poimirlem22  38603  poimirlem23  38604  broucube  38615  dvtan  38631  itg2addnc  38635  ibladdnc  38638  itgaddnc  38641  itgmulc2nclem2  38648  itgmulc2nc  38649  itgabsnc  38650  ftc1cnnclem  38652  ftc1anclem3  38656  ftc1anclem6  38659  ftc1anclem7  38660  ftc1anclem8  38661  dvasin  38665  dvacos  38666  dvreasin  38667  dvreacos  38668  areacirclem1  38669  areacirc  38674  fsumshftd  40052  hlrelat5N  40501  rhmzrhval  43065  aks6d1c1  43209  hashscontpow  43215  aks6d1c4  43217  aks6d1c2lem3  43219  aks6d1c2lem4  43220  aks6d1c2  43223  aks6d1c5lem0  43228  aks6d1c5lem3  43230  aks6d1c5lem2  43231  aks6d1c5  43232  sticksstones3  43241  sticksstones8  43246  sticksstones10  43248  sticksstones12a  43250  sticksstones12  43251  aks6d1c6lem1  43263  aks6d1c6lem2  43264  aks6d1c6lem3  43265  aks6d1c6lem4  43266  aks6d1c6isolem1  43267  aks6d1c6isolem2  43268  aks6d1c6isolem3  43269  aks6d1c6lem5  43270  aks6d1c7lem2  43274  unitscyglem1  43288  readvrec2  43455  readvrec  43456  readvcot  43458  frlmfzolen  43613  frlmfzoccat  43615  frlmvscadiccat  43616  evlsbagval  43657  evlselv  43660  fsuppind  43661  mhpind  43665  mhphflem  43667  prjspner  43690  prjspnvs  43691  frlmnzcoordex  43695  frlmnzcoordcl2  43699  frlmnzcoordsca  43701  prjspnnormval  43702  prjspnnorm  43704  0prjspnrel  43706  prjcrv0  43712  mzpclall  43780  mzpsubst  43801  eldioph2  43815  rabdiophlem2  43851  irrapxlem1  43871  mzpcong  44021  mendlmod  44233  naddcnff  44406  relexpmulnn  44751  iunrelexpuztr  44761  mnringvald  45253  mnringmulrvald  45267  radcnvrat  45340  hashnzfzclim  45348  lhe4.4ex1a  45355  expgrowthi  45359  expgrowth  45361  bccval  45364  binomcxplemrat  45376  binomcxplemfrat  45377  binomcxplemradcnv  45378  binomcxplemdvbinom  45379  binomcxplemdvsum  45381  binomcxplemnotnn0  45382  unirnmap  46263  unirnmapsn  46269  ssmapsn  46271  iocopn  46574  icoopn  46579  divcnvg  46681  sumnnodd  46684  climsubmpt  46712  dvsinax  46965  fperdvper  46971  dvdivf  46974  dvnprodlem1  46998  itgsincmulx  47026  stoweidlem59  47111  etransclem4  47290  etransclem13  47299  etransclem25  47311  etransclem48  47334  rrxtopnfi  47339  sge0tsms  47432  elhoi  47594  ovnval2  47597  ovnval2b  47604  ovncvrrp  47616  ovn0lem  47617  ovncl  47619  ovnome  47625  hoidmvlelem2  47648  hoidmvlelem3  47649  hoidmvle  47652  ovnlecvr2  47662  ovncvr2  47663  ovnsubadd2lem  47697  ovnovollem1  47708  vonvolmbl  47713  iunhoiioolem  47727  vonioolem1  47732  vonioolem2  47733  vonicclem2  47736  smfresal  47840  smfres  47842  smfmullem4  47846  smfco  47854  adddmmbl  47885  muldmmbl  47887  chnsuslle  47933  fmtno  48656  isubgruhgr  49008  grtriprop  49081  grtriclwlk3  49085  gpgvtx  49183  gpgiedg  49184  intopval  49341  clintopval  49343  rngchomALTV  49407  funcringcsetcALTV2lem5  49433  ringchomALTV  49441  funcringcsetclem5ALTV  49456  srhmsubcALTVlem2  49463  srhmsubcALTV  49464  fldhmsubcALTV  49472  zlmodzxzscm  49511  zlmodzxzadd  49512  rmsupp0  49522  domnmsuppn0  49523  rmsuppss  49524  ply1mulgsumlem3  49542  ply1mulgsumlem4  49543  ply1mulgsum  49544  dmatALTval  49554  lincop  49562  lincval  49563  linc1  49579  lincresunit3lem1  49633  fdivmpt  49694  fdivmptfv  49699  refdivmptfv  49700  digval  49752  2arymptfv  49804  2arymaptfo  49808  itcovalpclem1  49824  itcovalt2lem1  49829  ackvalsuc1mpt  49832  ackval1  49835  ackval2  49836  ackval3  49837  ackval42  49850  line2xlem  49907  upfval2  50327  swapfval  50412  tposcurf1  50449  tposcurf2val  50451  fucofvalg  50468  fuco112x  50482  fuco23  50491  fucoid  50498  fucocolem4  50506  prcofvalg  50526  prcof1  50538  opf2fval  50555  lanval  50769  ranval  50770  crosspdot0lem  51005  veroquadgsumlem  51025