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 2145  Vcvv 3451  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  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  33258  fsuppcurry1  33316  fsuppcurry2  33317  offinsupp1  33318  ressprs  33527  mntoval  33543  mgcoval  33547  mndlactf1  33587  mndlactfo  33588  mndractf1  33589  mndractfo  33590  mndlactf1o  33591  mndractf1o  33592  lmodvslmhm  33611  gsummulsubdishift2  33630  gsumwrd2dccat  33639  cycpmco2f1  33685  cycpmco2rn  33686  cycpmco2lem2  33688  cycpmco2lem3  33689  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2  33694  conjga  33731  cntrval2  33732  fxpsubm  33733  fxpsubg  33734  fxpsubrg  33735  fxpsdrg  33736  archirngz  33750  archiabllem2a  33755  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnsubrunlem2  33809  rlocval  33820  fracval  33866  quslmod  33919  quslmhm  33920  quslvec  33921  unitprodclb  33944  nsgmgc  33963  nsgqusf1olem1  33964  nsgqusf1olem2  33965  nsgqusf1olem3  33966  lmhmqusker  33968  rhmquskerlem  33975  elrspunidl  33978  opprqusbas  34012  opprqusplusg  34013  opprqusmulr  34015  opprqus1r  34016  qsdrngilem  34018  qsdrngi  34019  rprmdvdsprod  34066  1arithidomlem1  34067  1arithidomlem2  34068  1arithidom  34069  1arithufdlem3  34078  dfufd2lem  34081  zringfrac  34086  evl1deg1  34108  evl1deg2  34109  evl1deg3  34110  ply1gsumz  34131  r1plmhm  34141  0mplrim  34146  selvply1rhmlema  34150  selvply1rhmlemb  34151  selvply1rhmlem1  34152  selvply1rhmlem3  34154  selvply1rhmlem4  34155  selvply1rhmlem5  34156  mplvrpmrhm  34179  psrgsum  34180  psrmonmul  34182  psrmonprod  34184  mplgsum  34185  splyval  34191  esplyfval1  34205  esplyfvaln  34206  vietadeg1  34210  resssra  34219  ply1degltdimlem  34254  ply1degltdim  34255  qusdimsum  34260  fedgmullem1  34261  fedgmullem2  34262  fedgmul  34263  lactlmhm  34266  fldgenfldext  34300  evls1fldgencl  34302  fldextrspunlsplem  34305  fldextrspundgdvdslem  34312  fldextrspundgdvds  34313  extdgfialglem1  34324  extdgfialglem2  34325  algextdeglem4  34352  algextdeglem6  34354  algextdeglem7  34355  submateq  34441  lmatcl  34448  mdetpmtr1  34455  madjusmdetlem1  34459  madjusmdetlem3  34461  qqhvval  34615  esumfzf  34701  esumpfinvallem  34706  esumpmono  34711  esummulc1  34713  esumcvg  34718  esumgect  34722  ofcval  34731  omssubadd  34932  sitgfval  34973  sitmcl  34983  sseqfv2  35026  cndprobval  35065  ballotlemfval  35122  ballotlemsv  35142  ballotlemsf1o  35146  ofcccat  35175  signsplypnf  35179  signsply0  35180  signstfval  35193  signshf  35217  reprpmtf1o  35255  reprdifc  35256  logdivsqrle  35279  hgt750lemg  35283  hgt750lema  35286  lpadval  35308  cvmliftlem8  36057  cvmliftphtlem  36082  fmla1  36152  gonarlem  36159  sategoelfvb  36184  mrsubval  36274  ellcsrspsn  36406  r1peuqusdeg1  36408  fwddifval  36927  knoppcnlem1  37359  knoppcnlem6  37364  unbdqndv2lem2  37376  poimirlem1  38540  poimirlem2  38541  poimirlem3  38542  poimirlem5  38544  poimirlem6  38545  poimirlem7  38546  poimirlem10  38549  poimirlem11  38550  poimirlem12  38551  poimirlem16  38555  poimirlem19  38558  poimirlem22  38561  poimirlem23  38562  broucube  38573  dvtan  38589  itg2addnc  38593  ibladdnc  38596  itgaddnc  38599  itgmulc2nclem2  38606  itgmulc2nc  38607  itgabsnc  38608  ftc1cnnclem  38610  ftc1anclem3  38614  ftc1anclem6  38617  ftc1anclem7  38618  ftc1anclem8  38619  dvasin  38623  dvacos  38624  dvreasin  38625  dvreacos  38626  areacirclem1  38627  areacirc  38632  fsumshftd  40010  hlrelat5N  40459  rhmzrhval  43023  aks6d1c1  43167  hashscontpow  43173  aks6d1c4  43175  aks6d1c2lem3  43177  aks6d1c2lem4  43178  aks6d1c2  43181  aks6d1c5lem0  43186  aks6d1c5lem3  43188  aks6d1c5lem2  43189  aks6d1c5  43190  sticksstones3  43199  sticksstones8  43204  sticksstones10  43206  sticksstones12a  43208  sticksstones12  43209  aks6d1c6lem1  43221  aks6d1c6lem2  43222  aks6d1c6lem3  43223  aks6d1c6lem4  43224  aks6d1c6isolem1  43225  aks6d1c6isolem2  43226  aks6d1c6isolem3  43227  aks6d1c6lem5  43228  aks6d1c7lem2  43232  unitscyglem1  43246  readvrec2  43413  readvrec  43414  readvcot  43416  frlmfzolen  43571  frlmfzoccat  43573  frlmvscadiccat  43574  evlsbagval  43615  evlselv  43618  fsuppind  43619  mhpind  43623  mhphflem  43625  prjspner  43648  prjspnvs  43649  frlmnzcoordex  43653  frlmnzcoordcl2  43657  frlmnzcoordsca  43659  prjspnnormval  43660  prjspnnorm  43662  0prjspnrel  43664  prjcrv0  43670  mzpclall  43738  mzpsubst  43759  eldioph2  43773  rabdiophlem2  43809  irrapxlem1  43829  mzpcong  43979  mendlmod  44191  naddcnff  44364  relexpmulnn  44709  iunrelexpuztr  44719  mnringvald  45211  mnringmulrvald  45225  radcnvrat  45298  hashnzfzclim  45306  lhe4.4ex1a  45313  expgrowthi  45317  expgrowth  45319  bccval  45322  binomcxplemrat  45334  binomcxplemfrat  45335  binomcxplemradcnv  45336  binomcxplemdvbinom  45337  binomcxplemdvsum  45339  binomcxplemnotnn0  45340  unirnmap  46221  unirnmapsn  46227  ssmapsn  46229  iocopn  46532  icoopn  46537  divcnvg  46639  sumnnodd  46642  climsubmpt  46670  dvsinax  46923  fperdvper  46929  dvdivf  46932  dvnprodlem1  46956  itgsincmulx  46984  stoweidlem59  47069  etransclem4  47248  etransclem13  47257  etransclem25  47269  etransclem48  47292  rrxtopnfi  47297  sge0tsms  47390  elhoi  47552  ovnval2  47555  ovnval2b  47562  ovncvrrp  47574  ovn0lem  47575  ovncl  47577  ovnome  47583  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvle  47610  ovnlecvr2  47620  ovncvr2  47621  ovnsubadd2lem  47655  ovnovollem1  47666  vonvolmbl  47671  iunhoiioolem  47685  vonioolem1  47690  vonioolem2  47691  vonicclem2  47694  smfresal  47798  smfres  47800  smfmullem4  47804  smfco  47812  adddmmbl  47843  muldmmbl  47845  chnsuslle  47891  fmtno  48614  isubgruhgr  48966  grtriprop  49039  grtriclwlk3  49043  gpgvtx  49141  gpgiedg  49142  intopval  49299  clintopval  49301  rngchomALTV  49365  funcringcsetcALTV2lem5  49391  ringchomALTV  49399  funcringcsetclem5ALTV  49414  srhmsubcALTVlem2  49421  srhmsubcALTV  49422  fldhmsubcALTV  49430  zlmodzxzscm  49469  zlmodzxzadd  49470  rmsupp0  49480  domnmsuppn0  49481  rmsuppss  49482  ply1mulgsumlem3  49500  ply1mulgsumlem4  49501  ply1mulgsum  49502  dmatALTval  49512  lincop  49520  lincval  49521  linc1  49537  lincresunit3lem1  49591  fdivmpt  49652  fdivmptfv  49657  refdivmptfv  49658  digval  49710  2arymptfv  49762  2arymaptfo  49766  itcovalpclem1  49782  itcovalt2lem1  49787  ackvalsuc1mpt  49790  ackval1  49793  ackval2  49794  ackval3  49795  ackval42  49808  line2xlem  49865  upfval2  50285  swapfval  50370  tposcurf1  50407  tposcurf2val  50409  fucofvalg  50426  fuco112x  50440  fuco23  50449  fucoid  50456  fucocolem4  50464  prcofvalg  50484  prcof1  50496  opf2fval  50513  lanval  50727  ranval  50728  crosspdot0lem  50963  veroquadgsumlem  50983