Theorem ovexd 7451

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453  (class class class)co 7416

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-sn 4588  df-pr 4590  df-uni 4871  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  caofidlcan  7719  caofass  7721  caofdi  7723  caofdir  7724  caonncan  7725  suppofssd  8204  mapsnend  9046  snmapen  9048  pw2eng  9084  mapen  9142  mapxpen  9144  mapunen  9147  mapdom2  9149  cantnfcl  9649  cantnfle  9653  cantnflt  9654  cantnflt2  9655  cantnfp1lem2  9661  cantnfp1lem3  9662  cantnflem1b  9668  cantnflem1d  9670  cantnflem1  9671  cnfcomlem  9681  cnfcom  9682  cnfcom2lem  9683  cnfcom3lem  9685  fzen  13597  seqf1o  14109  wrdexg  14591  wrdnval  14612  pfxval  14745  pfxswrd  14777  splval  14822  s3rex  15023  s3rexrd  15024  ofccat  15044  climshftlem  15663  climshft  15665  climshft2  15671  caucvgr  15765  fsumrev  15867  hashdvds  16870  setsabs  17275  ressress  17343  firest  17521  prdsvscafval  17569  qusval  17632  xpsbas  17662  xpsadd  17664  xpsmul  17665  xpssca  17666  xpsvsca  17667  xpsless  17668  xpsle  17669  homfval  17784  comfval  17792  cicfval  17890  rescabs  17926  rescabs2  17927  resscat  17945  funcres2c  17996  ressffth  18033  fucbas  18056  fuccoval  18059  setchom  18173  catchom  18196  catcco  18198  estrchom  18219  funcestrcsetclem5  18236  funcsetcestrclem5  18251  evlf2val  18311  curf11  18318  curf12  18319  curf2val  18322  uncfval  18326  diagval  18332  hof2  18349  yonval  18353  resspos  18521  gsumval2a  18789  gsumval2  18790  mndpsuppss  18874  gsumwspan  18956  efmnd  18980  qustriv  19310  qustrivr  19311  ghmqusnsglem1  19408  ghmqusnsglem2  19409  ghmqusnsg  19410  ghmquskerlem1  19411  ghmquskerco  19412  ghmquskerlem2  19413  ghmquskerlem3  19414  ghmqusker  19415  orbstafun  19439  orbstaval  19440  symgval  19499  psgnvalii  19637  lsmhash  19833  frgpupval  19902  qusabl  19993  gsumval3  20035  gsumreidx  20045  gsumzaddlem  20049  gsummptshft  20064  telgsumfzslem  20116  telgsumfz  20118  telgsumfz0  20120  dpjval  20186  prdsrngd  20312  srgbinomlem3  20368  srgbinomlem4  20369  mulgass3  20495  rngcval  20781  rnghmsscmap2  20792  rnghmsscmap  20793  funcrngcsetc  20803  ringcval  20810  rhmsscmap2  20821  rhmsscmap  20822  funcringcsetc  20837  srhmsubclem3  20842  srhmsubc  20843  fldhmsubc  20952  lcomfsupp  21087  rmodislmodlem  21114  rmodislmod  21115  sraval  21360  srasca  21365  crngridl  21483  quscrng  21487  rhmqusnsg  21489  qsidomlem1  21544  qsidomlem2  21545  pzriprnglem11  21705  znval  21749  znzrhfo  21761  znunithash  21778  cygznlem2  21782  frobrhm  21789  pjfval  21920  pjpm  21922  frlmgsum  21986  frlmipval  21993  frlmphllem  21994  frlmphl  21995  frlmsslsp  22010  frlmup1  22012  gsumbagdiaglem  22147  psrass1lem  22149  rhmpsrlem1  22156  psrass1  22179  psrdi  22180  psrdir  22181  psrass23l  22182  psrascl  22194  mplval  22204  mplsubglem  22214  mplsubrglem  22219  mplmonmul  22253  mplcoe1  22254  opsrval  22263  psrbagev1  22294  psrbagev2  22295  evlslem6  22298  evlslem1  22299  evlsval  22303  evlsval3  22306  evlsvval  22307  evlsvvval  22310  evlcl  22319  evladdval  22320  evlmulval  22321  mpfconst  22326  mpff  22329  mpfaddcl  22330  mpfmulcl  22331  mpfind  22332  mhmcompl  22338  mhmcoaddmpl  22340  evlscl  22342  evlsexpval  22345  evlsaddval  22346  evlsmulval  22347  evlsevl  22349  selvcl  22357  mhpmulcl  22378  mhpaddcl  22380  psdcoef  22389  psdmplcl  22391  psdadd  22392  ply1lss  22422  gsumply1subr  22459  coe1add  22491  coe1tm  22500  coe1tmmul  22504  cply1mul  22522  ply1coe  22524  evl1expd  22571  pf1mpf  22578  pf1ind  22581  rhmmpl  22606  rhmply1vsca  22611  mamufv  22617  mamuass  22625  mamuvs1  22628  mamuvs2  22629  matgsum  22660  dmatmul  22720  scmatval  22727  scmatrhmval  22750  mvmulfv  22767  mavmulfv  22769  mavmulass  22772  marrepeval  22786  marepveval  22791  submaeval  22805  mdetrsca  22826  mdetunilem9  22843  mdetuni0  22844  gsummatr01lem3  22880  gsummatr01lem4  22881  gsummatr01  22882  smadiadetlem3  22891  cramerlem1  22913  mat2pmatmul  22957  m2cpminvid  22979  decpmatfsupp  22995  decpmatmullem  22997  decpmatmul  22998  decpmatmulsumfsupp  22999  pmatcollpw1lem1  23000  pmatcollpw3fi1lem1  23012  pmatcollpwscmatlem2  23016  pm2mpfval  23022  pm2mpf  23024  mply1topmatcllem  23029  mp2pm2mplem3  23034  mp2pm2mplem4  23035  pm2mpmhmlem1  23044  pm2mpmhmlem2  23045  pm2mp  23051  chfacfscmulfsupp  23085  chfacfscmulgsum  23086  chfacfpmmulfsupp  23089  chfacfpmmulgsum  23090  cpmidpmatlem3  23098  cpmadugsumlemB  23100  cpmadugsumlemC  23101  cpmadugsumlemF  23102  cayhamlem4  23114  xpstopnlem2  24038  fcfval  24260  tsmsxplem1  24380  tsmsxplem2  24381  tusval  24492  xpsdsfn  24604  xpsxmet  24607  xpsdsval  24608  xpsmet  24609  tmsval  24708  met1stc  24748  metuval  24776  cnmpopc  25157  pi1val  25266  pi1addf  25276  pi1addval  25277  pi1grplem  25278  rrxnm  25620  rrxcph  25621  rrxmval  25634  mbfmulc2  25892  mbfmul  25955  itg2mulclem  25975  ibladd  26050  itgadd  26054  itgabs  26064  bddmulibl  26068  dvmulf  26172  dvcmulf  26174  dvmptmul  26190  cmvth  26220  dvlip  26222  ftc1lem4  26268  mdegmullem  26305  coe1mul3  26326  r1pval  26385  plyco  26468  dgrcolem1  26500  elqaalem3  26552  taylpfval  26598  taylthlem2  26607  pserdvlem2  26661  advlogexp  26890  logtayl  26895  logccv  26898  dvcxp1  26975  dvcncxp1  26978  logbmpt  27023  logbfval  27025  relogbf  27026  dvatan  27170  cxp2lim  27211  cxploglim2  27213  lgamgulmlem2  27264  lgamgulm2  27270  lgamcvglem  27274  lgamf  27276  basellem7  27321  basellem8  27322  basellem9  27323  fsumdvdscom  27419  logexprlim  27459  dchrfi  27489  gausslemma2dlem2  27601  gausslemma2dlem3  27602  2lgslem1b  27626  chtppilimlem2  27708  chebbnd2  27711  chto1lb  27712  chpchtlim  27713  chpo1ub  27714  vmadivsum  27716  dchrisum0lem3  27753  mudivsum  27764  logdivsum  27767  log2sumbnd  27778  selberglem1  27779  selberg2lem  27784  selberg2  27785  selbergr  27802  negsval  28288  wlkp1  30125  cyclnumvtx  30253  wwlksnextsurj  30354  wwlksnextbij  30356  clwlkclwwlklem2a1  30448  clwlkclwwlkf1  30466  eupth2eucrct  30683  frgrncvvdeq  30775  numclwlk2lem2fv  30844  numclwwlk2lem3  30846  ofoprabco  33124  fsuppcurry1  33182  fsuppcurry2  33183  offinsupp1  33184  ressprs  33393  mntoval  33409  mgcoval  33413  mndlactf1  33453  mndlactfo  33454  mndractf1  33455  mndractfo  33456  mndlactf1o  33457  mndractf1o  33458  lmodvslmhm  33477  gsummulsubdishift2  33496  gsumwrd2dccat  33505  cycpmco2f1  33551  cycpmco2rn  33552  cycpmco2lem2  33554  cycpmco2lem3  33555  cycpmco2lem4  33556  cycpmco2lem5  33557  cycpmco2lem6  33558  cycpmco2  33560  conjga  33597  cntrval2  33598  fxpsubm  33599  fxpsubg  33600  fxpsubrg  33601  fxpsdrg  33602  archirngz  33616  archiabllem2a  33621  elrgspnlem1  33669  elrgspnlem2  33670  elrgspnsubrunlem2  33675  rlocval  33686  fracval  33732  quslmod  33785  quslmhm  33786  quslvec  33787  unitprodclb  33809  nsgmgc  33828  nsgqusf1olem1  33829  nsgqusf1olem2  33830  nsgqusf1olem3  33831  lmhmqusker  33833  rhmquskerlem  33840  elrspunidl  33843  opprqusbas  33877  opprqusplusg  33878  opprqusmulr  33880  opprqus1r  33881  qsdrngilem  33883  qsdrngi  33884  rprmdvdsprod  33931  1arithidomlem1  33932  1arithidomlem2  33933  1arithidom  33934  1arithufdlem3  33943  dfufd2lem  33946  zringfrac  33951  evl1deg1  33973  evl1deg2  33974  evl1deg3  33975  ply1gsumz  33996  r1plmhm  34006  0mplrim  34011  selvply1rhmlema  34015  selvply1rhmlemb  34016  selvply1rhmlem1  34017  selvply1rhmlem3  34019  selvply1rhmlem4  34020  selvply1rhmlem5  34021  mplvrpmrhm  34044  psrgsum  34045  psrmonmul  34047  psrmonprod  34049  mplgsum  34050  splyval  34056  esplyfval1  34070  esplyfvaln  34071  vietadeg1  34075  resssra  34084  ply1degltdimlem  34119  ply1degltdim  34120  qusdimsum  34125  fedgmullem1  34126  fedgmullem2  34127  fedgmul  34128  lactlmhm  34131  fldgenfldext  34165  evls1fldgencl  34167  fldextrspunlsplem  34170  fldextrspundgdvdslem  34177  fldextrspundgdvds  34178  extdgfialglem1  34189  extdgfialglem2  34190  algextdeglem4  34217  algextdeglem6  34219  algextdeglem7  34220  submateq  34306  lmatcl  34313  mdetpmtr1  34320  madjusmdetlem1  34324  madjusmdetlem3  34326  qqhvval  34480  esumfzf  34566  esumpfinvallem  34571  esumpmono  34576  esummulc1  34578  esumcvg  34583  esumgect  34587  ofcval  34596  omssubadd  34798  sitgfval  34839  sitmcl  34849  sseqfv2  34892  cndprobval  34931  ballotlemfval  34988  ballotlemsv  35008  ballotlemsf1o  35012  ofcccat  35041  signsplypnf  35045  signsply0  35046  signstfval  35059  signshf  35083  reprpmtf1o  35121  reprdifc  35122  logdivsqrle  35145  hgt750lemg  35149  hgt750lema  35152  lpadval  35174  cvmliftlem8  35858  cvmliftphtlem  35883  fmla1  35953  gonarlem  35960  sategoelfvb  35985  mrsubval  36075  ellcsrspsn  36207  r1peuqusdeg1  36209  fwddifval  36729  knoppcnlem1  37177  knoppcnlem6  37182  unbdqndv2lem2  37194  poimirlem1  38357  poimirlem2  38358  poimirlem3  38359  poimirlem5  38361  poimirlem6  38362  poimirlem7  38363  poimirlem10  38366  poimirlem11  38367  poimirlem12  38368  poimirlem16  38372  poimirlem19  38375  poimirlem22  38378  poimirlem23  38379  broucube  38390  dvtan  38406  itg2addnc  38410  ibladdnc  38413  itgaddnc  38416  itgmulc2nclem2  38423  itgmulc2nc  38424  itgabsnc  38425  ftc1cnnclem  38427  ftc1anclem3  38431  ftc1anclem6  38434  ftc1anclem7  38435  ftc1anclem8  38436  dvasin  38440  dvacos  38441  dvreasin  38442  dvreacos  38443  areacirclem1  38444  areacirc  38449  fsumshftd  39812  hlrelat5N  40261  rhmzrhval  42825  aks6d1c1  42969  hashscontpow  42975  aks6d1c4  42977  aks6d1c2lem3  42979  aks6d1c2lem4  42980  aks6d1c2  42983  aks6d1c5lem0  42988  aks6d1c5lem3  42990  aks6d1c5lem2  42991  aks6d1c5  42992  sticksstones3  43001  sticksstones8  43006  sticksstones10  43008  sticksstones12a  43010  sticksstones12  43011  aks6d1c6lem1  43023  aks6d1c6lem2  43024  aks6d1c6lem3  43025  aks6d1c6lem4  43026  aks6d1c6isolem1  43027  aks6d1c6isolem2  43028  aks6d1c6isolem3  43029  aks6d1c6lem5  43030  aks6d1c7lem2  43034  unitscyglem1  43048  readvrec2  43223  readvrec  43224  readvcot  43226  frlmfzolen  43378  frlmfzoccat  43380  frlmvscadiccat  43381  evlsbagval  43419  evlselv  43422  fsuppind  43423  mhpind  43427  mhphflem  43429  prjspner  43452  prjspnvs  43453  prjspnfv01  43457  prjspner01  43458  prjspner1  43459  0prjspnrel  43460  prjcrv0  43466  mzpclall  43559  mzpsubst  43580  eldioph2  43594  rabdiophlem2  43630  irrapxlem1  43650  mzpcong  43800  mendlmod  44017  naddcnff  44190  relexpmulnn  44536  iunrelexpuztr  44546  mnringvald  45038  mnringmulrvald  45052  radcnvrat  45125  hashnzfzclim  45133  lhe4.4ex1a  45140  expgrowthi  45144  expgrowth  45146  bccval  45149  binomcxplemrat  45161  binomcxplemfrat  45162  binomcxplemradcnv  45163  binomcxplemdvbinom  45164  binomcxplemdvsum  45166  binomcxplemnotnn0  45167  unirnmap  46025  unirnmapsn  46031  ssmapsn  46033  iocopn  46337  icoopn  46342  divcnvg  46444  sumnnodd  46447  climsubmpt  46475  dvsinax  46728  fperdvper  46734  dvdivf  46737  dvnprodlem1  46761  itgsincmulx  46789  stoweidlem59  46874  etransclem4  47053  etransclem13  47062  etransclem25  47074  etransclem48  47097  rrxtopnfi  47102  sge0tsms  47195  elhoi  47357  ovnval2  47360  ovnval2b  47367  ovncvrrp  47379  ovn0lem  47380  ovncl  47382  ovnome  47388  hoidmvlelem2  47411  hoidmvlelem3  47412  hoidmvle  47415  ovnlecvr2  47425  ovncvr2  47426  ovnsubadd2lem  47460  ovnovollem1  47471  vonvolmbl  47476  iunhoiioolem  47490  vonioolem1  47495  vonioolem2  47496  vonicclem2  47499  smfresal  47603  smfres  47605  smfmullem4  47609  smfco  47617  adddmmbl  47648  muldmmbl  47650  chnsuslle  47696  fmtno  48419  isubgruhgr  48771  grtriprop  48844  grtriclwlk3  48848  gpgvtx  48946  gpgiedg  48947  intopval  49104  clintopval  49106  rngchomALTV  49170  funcringcsetcALTV2lem5  49196  ringchomALTV  49204  funcringcsetclem5ALTV  49219  srhmsubcALTVlem2  49226  srhmsubcALTV  49227  fldhmsubcALTV  49235  zlmodzxzscm  49274  zlmodzxzadd  49275  rmsupp0  49285  domnmsuppn0  49286  rmsuppss  49287  ply1mulgsumlem3  49305  ply1mulgsumlem4  49306  ply1mulgsum  49307  dmatALTval  49317  lincop  49325  lincval  49326  linc1  49342  lincresunit3lem1  49396  fdivmpt  49457  fdivmptfv  49462  refdivmptfv  49463  digval  49515  2arymptfv  49567  2arymaptfo  49571  itcovalpclem1  49587  itcovalt2lem1  49592  ackvalsuc1mpt  49595  ackval1  49598  ackval2  49599  ackval3  49600  ackval42  49613  line2xlem  49670  upfval2  50090  swapfval  50175  tposcurf1  50212  tposcurf2val  50214  fucofvalg  50231  fuco112x  50245  fuco23  50254  fucoid  50261  fucocolem4  50269  prcofvalg  50289  prcof1  50301  opf2fval  50318  lanval  50532  ranval  50533  crosspdot0lem  50783  veroquadgsumlem  50803