Theorem ovexd 7381

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  (class class class)co 7346

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5242

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-sn 4574  df-pr 4576  df-uni 4857  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  caofidlcan  7648  caofass  7650  caofdi  7652  caofdir  7653  caonncan  7654  suppofssd  8133  mapsnend  8958  snmapen  8960  pw2eng  8996  mapen  9054  mapxpen  9056  mapunen  9059  mapdom2  9061  cantnfcl  9557  cantnfle  9561  cantnflt  9562  cantnflt2  9563  cantnfp1lem2  9569  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1d  9578  cantnflem1  9579  cnfcomlem  9589  cnfcom  9590  cnfcom2lem  9591  cnfcom3lem  9593  fzen  13441  seqf1o  13950  wrdexg  14431  wrdnval  14452  pfxval  14581  pfxswrd  14613  splval  14658  ofccat  14876  climshftlem  15481  climshft  15483  climshft2  15489  caucvgr  15583  fsumrev  15686  hashdvds  16686  setsabs  17090  ressress  17158  firest  17336  prdsvscafval  17384  qusval  17446  xpsbas  17476  xpsadd  17478  xpsmul  17479  xpssca  17480  xpsvsca  17481  xpsless  17482  xpsle  17483  homfval  17598  comfval  17606  cicfval  17704  rescabs  17740  rescabs2  17741  resscat  17759  funcres2c  17810  ressffth  17847  fucbas  17870  fuccoval  17873  setchom  17987  catchom  18010  catcco  18012  estrchom  18033  funcestrcsetclem5  18050  funcsetcestrclem5  18065  evlf2val  18125  curf11  18132  curf12  18133  curf2val  18136  uncfval  18140  diagval  18146  hof2  18163  yonval  18167  resspos  18335  gsumval2a  18593  gsumval2  18594  mndpsuppss  18673  gsumwspan  18754  efmnd  18778  ghmqusnsglem1  19192  ghmqusnsglem2  19193  ghmqusnsg  19194  ghmquskerlem1  19195  ghmquskerco  19196  ghmquskerlem2  19197  ghmquskerlem3  19198  ghmqusker  19199  orbstafun  19223  orbstaval  19224  symgval  19283  psgnvalii  19421  lsmhash  19617  frgpupval  19686  qusabl  19777  gsumval3  19819  gsumreidx  19829  gsumzaddlem  19833  gsummptshft  19848  telgsumfzslem  19900  telgsumfz  19902  telgsumfz0  19904  dpjval  19970  prdsrngd  20094  srgbinomlem3  20146  srgbinomlem4  20147  mulgass3  20271  rngcval  20533  rnghmsscmap2  20544  rnghmsscmap  20545  funcrngcsetc  20555  ringcval  20562  rhmsscmap2  20573  rhmsscmap  20574  funcringcsetc  20589  srhmsubclem3  20594  srhmsubc  20595  fldhmsubc  20700  lcomfsupp  20835  rmodislmodlem  20862  rmodislmod  20863  sraval  21109  srasca  21114  crngridl  21217  quscrng  21220  rhmqusnsg  21222  pzriprnglem11  21428  znval  21472  znzrhfo  21484  znunithash  21501  cygznlem2  21505  frobrhm  21512  pjfval  21643  pjpm  21645  frlmgsum  21709  frlmipval  21716  frlmphllem  21717  frlmphl  21718  frlmsslsp  21733  frlmup1  21735  gsumbagdiaglem  21867  psrass1lem  21869  rhmpsrlem1  21877  psrass1  21901  psrdi  21902  psrdir  21903  psrass23l  21904  psrascl  21916  mplval  21926  mplsubglem  21936  mplsubrglem  21941  mplmonmul  21971  mplcoe1  21972  opsrval  21981  psrbagev1  22012  psrbagev2  22013  evlslem6  22016  evlslem1  22017  evlsval  22021  mpfconst  22036  mpff  22039  mpfaddcl  22040  mpfmulcl  22041  mpfind  22042  mhpmulcl  22064  mhpaddcl  22066  psdcoef  22075  psdmplcl  22077  psdadd  22078  ply1lss  22109  gsumply1subr  22146  coe1add  22178  coe1tm  22187  coe1tmmul  22191  cply1mul  22211  ply1coe  22213  evl1expd  22260  pf1mpf  22267  pf1ind  22270  mhmcompl  22295  mhmcoaddmpl  22296  rhmmpl  22298  rhmply1vsca  22303  mamufv  22309  mamuass  22317  mamuvs1  22320  mamuvs2  22321  matgsum  22352  dmatmul  22412  scmatval  22419  scmatrhmval  22442  mvmulfv  22459  mavmulfv  22461  mavmulass  22464  marrepeval  22478  marepveval  22483  submaeval  22497  mdetrsca  22518  mdetunilem9  22535  mdetuni0  22536  gsummatr01lem3  22572  gsummatr01lem4  22573  gsummatr01  22574  smadiadetlem3  22583  cramerlem1  22602  mat2pmatmul  22646  m2cpminvid  22668  decpmatfsupp  22684  decpmatmullem  22686  decpmatmul  22687  decpmatmulsumfsupp  22688  pmatcollpw1lem1  22689  pmatcollpw3fi1lem1  22701  pmatcollpwscmatlem2  22705  pm2mpfval  22711  pm2mpf  22713  mply1topmatcllem  22718  mp2pm2mplem3  22723  mp2pm2mplem4  22724  pm2mpmhmlem1  22733  pm2mpmhmlem2  22734  pm2mp  22740  chfacfscmulfsupp  22774  chfacfscmulgsum  22775  chfacfpmmulfsupp  22778  chfacfpmmulgsum  22779  cpmidpmatlem3  22787  cpmadugsumlemB  22789  cpmadugsumlemC  22790  cpmadugsumlemF  22791  cayhamlem4  22803  xpstopnlem2  23726  fcfval  23948  tsmsxplem1  24068  tsmsxplem2  24069  tusval  24180  xpsdsfn  24292  xpsxmet  24295  xpsdsval  24296  xpsmet  24297  tmsval  24396  met1stc  24436  metuval  24464  cnmpopc  24849  pi1val  24964  pi1addf  24974  pi1addval  24975  pi1grplem  24976  rrxnm  25318  rrxcph  25319  rrxmval  25332  mbfmulc2  25591  mbfmul  25654  itg2mulclem  25674  ibladd  25749  itgadd  25753  itgabs  25763  bddmulibl  25767  dvmulf  25873  dvcmulf  25875  dvmptmul  25892  cmvth  25922  dvlip  25925  ftc1lem4  25973  mdegmullem  26010  coe1mul3  26031  r1pval  26090  plyco  26173  dgrcolem1  26206  elqaalem3  26256  taylpfval  26299  taylthlem2  26309  taylthlem2OLD  26310  pserdvlem2  26365  advlogexp  26591  logtayl  26596  logccv  26599  dvcxp1  26676  dvcncxp1  26679  logbmpt  26725  logbfval  26727  relogbf  26728  dvatan  26872  cxp2lim  26914  cxploglim2  26916  lgamgulmlem2  26967  lgamgulm2  26973  lgamcvglem  26977  lgamf  26979  basellem7  27024  basellem8  27025  basellem9  27026  fsumdvdscom  27122  logexprlim  27163  dchrfi  27193  gausslemma2dlem2  27305  gausslemma2dlem3  27306  2lgslem1b  27330  chtppilimlem2  27412  chebbnd2  27415  chto1lb  27416  chpchtlim  27417  chpo1ub  27418  vmadivsum  27420  dchrisum0lem3  27457  mudivsum  27468  logdivsum  27471  log2sumbnd  27482  selberglem1  27483  selberg2lem  27488  selberg2  27489  selbergr  27506  negsval  27967  wlkp1  29658  cyclnumvtx  29778  wwlksnextsurj  29878  wwlksnextbij  29880  clwlkclwwlklem2a1  29972  clwlkclwwlkf1  29990  eupth2eucrct  30197  frgrncvvdeq  30289  numclwlk2lem2fv  30358  numclwwlk2lem3  30360  ofoprabco  32646  fsuppcurry1  32707  fsuppcurry2  32708  offinsupp1  32709  ressprs  32947  mntoval  32963  mgcoval  32967  mndlactf1  33007  mndlactfo  33008  mndractf1  33009  mndractfo  33010  mndlactf1o  33011  mndractf1o  33012  lmodvslmhm  33030  gsumwrd2dccat  33047  cycpmco2f1  33093  cycpmco2rn  33094  cycpmco2lem2  33096  cycpmco2lem3  33097  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2  33102  conjga  33139  cntrval2  33140  fxpsubm  33141  fxpsubg  33142  fxpsubrg  33143  fxpsdrg  33144  archirngz  33158  archiabllem2a  33163  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnsubrunlem2  33215  rlocval  33226  fracval  33270  quslmod  33323  quslmhm  33324  quslvec  33325  qustriv  33329  qustrivr  33330  unitprodclb  33354  nsgmgc  33377  nsgqusf1olem1  33378  nsgqusf1olem2  33379  nsgqusf1olem3  33380  lmhmqusker  33382  rhmquskerlem  33390  elrspunidl  33393  qsidomlem1  33417  qsidomlem2  33418  opprqusbas  33453  opprqusplusg  33454  opprqusmulr  33456  opprqus1r  33457  qsdrngilem  33459  qsdrngi  33460  rprmdvdsprod  33499  1arithidomlem1  33500  1arithidomlem2  33501  1arithidom  33502  1arithufdlem3  33511  dfufd2lem  33514  zringfrac  33519  evl1deg1  33539  evl1deg2  33540  evl1deg3  33541  ply1gsumz  33559  r1plmhm  33570  mplvrpmrhm  33577  splyval  33582  resssra  33599  ply1degltdimlem  33635  ply1degltdim  33636  qusdimsum  33641  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  lactlmhm  33647  fldgenfldext  33681  evls1fldgencl  33683  fldextrspunlsplem  33686  fldextrspundgdvdslem  33693  fldextrspundgdvds  33694  extdgfialglem1  33705  extdgfialglem2  33706  extdgfialg  33707  algextdeglem4  33733  algextdeglem6  33735  algextdeglem7  33736  submateq  33822  lmatcl  33829  mdetpmtr1  33836  madjusmdetlem1  33840  madjusmdetlem3  33842  qqhvval  33996  esumfzf  34082  esumpfinvallem  34087  esumpmono  34092  esummulc1  34094  esumcvg  34099  esumgect  34103  ofcval  34112  omssubadd  34313  sitgfval  34354  sitmcl  34364  sseqfv2  34407  cndprobval  34446  ballotlemfval  34503  ballotlemsv  34523  ballotlemsf1o  34527  ofcccat  34556  signsplypnf  34563  signsply0  34564  signstfval  34577  signshf  34601  reprpmtf1o  34639  reprdifc  34640  logdivsqrle  34663  hgt750lemg  34667  hgt750lema  34670  lpadval  34689  cvmliftlem8  35336  cvmliftphtlem  35361  fmla1  35431  gonarlem  35438  sategoelfvb  35463  mrsubval  35553  ellcsrspsn  35685  r1peuqusdeg1  35687  fwddifval  36206  knoppcnlem1  36537  knoppcnlem6  36542  unbdqndv2lem2  36554  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem5  37664  poimirlem6  37665  poimirlem7  37666  poimirlem10  37669  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem19  37678  poimirlem22  37681  poimirlem23  37682  broucube  37693  dvtan  37709  itg2addnc  37713  ibladdnc  37716  itgaddnc  37719  itgmulc2nclem2  37726  itgmulc2nc  37727  itgabsnc  37728  ftc1cnnclem  37730  ftc1anclem3  37734  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  dvasin  37743  dvacos  37744  dvreasin  37745  dvreacos  37746  areacirclem1  37747  areacirc  37752  fsumshftd  39050  hlrelat5N  39499  rhmzrhval  42063  aks6d1c1  42208  hashscontpow  42214  aks6d1c4  42216  aks6d1c2lem3  42218  aks6d1c2lem4  42219  aks6d1c2  42222  aks6d1c5lem0  42227  aks6d1c5lem3  42229  aks6d1c5lem2  42230  aks6d1c5  42231  sticksstones3  42240  sticksstones8  42245  sticksstones10  42247  sticksstones12a  42249  sticksstones12  42250  aks6d1c6lem1  42262  aks6d1c6lem2  42263  aks6d1c6lem3  42264  aks6d1c6lem4  42265  aks6d1c6isolem1  42266  aks6d1c6isolem2  42267  aks6d1c6isolem3  42268  aks6d1c6lem5  42269  aks6d1c7lem2  42273  unitscyglem1  42287  readvrec2  42453  readvrec  42454  readvcot  42456  frlmfzolen  42595  frlmfzoccat  42597  frlmvscadiccat  42598  evlscl  42650  evlsval3  42651  evlsvval  42652  evlsvvval  42655  evlsbagval  42658  evlsexpval  42659  evlsaddval  42660  evlsmulval  42661  evlsevl  42663  evlcl  42664  evladdval  42667  evlmulval  42668  selvcl  42675  evlselv  42679  fsuppind  42682  mhpind  42686  mhphflem  42688  prjspner  42711  prjspnvs  42712  prjspnfv01  42716  prjspner01  42717  prjspner1  42718  0prjspnrel  42719  prjcrv0  42725  mzpclall  42819  mzpsubst  42840  eldioph2  42854  rabdiophlem2  42894  irrapxlem1  42914  mzpcong  43064  mendlmod  43281  naddcnff  43454  relexpmulnn  43801  iunrelexpuztr  43811  mnringvald  44305  mnringmulrvald  44319  radcnvrat  44406  hashnzfzclim  44414  lhe4.4ex1a  44421  expgrowthi  44425  expgrowth  44427  bccval  44430  binomcxplemrat  44442  binomcxplemfrat  44443  binomcxplemradcnv  44444  binomcxplemdvbinom  44445  binomcxplemdvsum  44447  binomcxplemnotnn0  44448  unirnmap  45304  unirnmapsn  45310  ssmapsn  45312  iocopn  45619  icoopn  45624  divcnvg  45726  sumnnodd  45729  climsubmpt  45757  dvsinax  46010  fperdvper  46016  dvdivf  46019  dvnprodlem1  46043  itgsincmulx  46071  stoweidlem59  46156  etransclem4  46335  etransclem13  46344  etransclem25  46356  etransclem48  46379  rrxtopnfi  46384  sge0tsms  46477  elhoi  46639  ovnval2  46642  ovnval2b  46649  ovncvrrp  46661  ovn0lem  46662  ovncl  46664  ovnome  46670  hoidmvlelem2  46693  hoidmvlelem3  46694  hoidmvle  46697  ovnlecvr2  46707  ovncvr2  46708  ovnsubadd2lem  46742  ovnovollem1  46753  vonvolmbl  46758  iunhoiioolem  46772  vonioolem1  46777  vonioolem2  46778  vonicclem2  46781  smfresal  46885  smfres  46887  smfmullem4  46891  smfco  46899  adddmmbl  46930  muldmmbl  46932  chnsuslle  46978  nthrucw  46983  sinnpoly  46990  fmtno  47628  isubgruhgr  47967  grtriprop  48040  grtriclwlk3  48044  gpgvtx  48142  gpgiedg  48143  intopval  48301  clintopval  48303  rngchomALTV  48367  funcringcsetcALTV2lem5  48393  ringchomALTV  48401  funcringcsetclem5ALTV  48416  srhmsubcALTVlem2  48423  srhmsubcALTV  48424  fldhmsubcALTV  48432  zlmodzxzscm  48456  zlmodzxzadd  48457  rmsupp0  48467  domnmsuppn0  48468  rmsuppss  48469  ply1mulgsumlem3  48488  ply1mulgsumlem4  48489  ply1mulgsum  48490  dmatALTval  48500  lincop  48508  lincval  48509  linc1  48525  lincresunit3lem1  48579  fdivmpt  48640  fdivmptfv  48645  refdivmptfv  48646  digval  48698  2arymptfv  48750  2arymaptfo  48754  itcovalpclem1  48770  itcovalt2lem1  48775  ackvalsuc1mpt  48778  ackval1  48781  ackval2  48782  ackval3  48783  ackval42  48796  line2xlem  48853  upfval2  49277  swapfval  49362  tposcurf1  49399  tposcurf2val  49401  fucofvalg  49418  fuco112x  49432  fuco23  49441  fucoid  49448  fucocolem4  49456  prcofvalg  49476  prcof1  49488  opf2fval  49505  lanval  49719  ranval  49720