Theorem ovexd 7466

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  caofidlcan  7735  caofass  7737  caofdi  7739  caofdir  7740  caonncan  7741  suppofssd  8228  mapsnend  9076  snmapen  9078  pw2eng  9118  mapen  9181  mapxpen  9183  mapunen  9186  mapdom2  9188  cantnfcl  9707  cantnfle  9711  cantnflt  9712  cantnflt2  9713  cantnfp1lem2  9719  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1d  9728  cantnflem1  9729  cnfcomlem  9739  cnfcom  9740  cnfcom2lem  9741  cnfcom3lem  9743  fzen  13581  seqf1o  14084  wrdexg  14562  wrdnval  14583  pfxval  14711  pfxswrd  14744  splval  14789  cshwsexaOLD  14863  ofccat  15008  climshftlem  15610  climshft  15612  climshft2  15618  caucvgr  15712  fsumrev  15815  hashdvds  16812  setsabs  17216  ressress  17293  firest  17477  prdsvscafval  17525  qusval  17587  xpsbas  17617  xpsadd  17619  xpsmul  17620  xpssca  17621  xpsvsca  17622  xpsless  17623  xpsle  17624  homfval  17735  comfval  17743  cicfval  17841  rescabs  17877  rescabsOLD  17878  rescabs2  17879  resscat  17897  funcres2c  17948  ressffth  17985  fucbas  18008  fuccoval  18011  setchom  18125  catchom  18148  catcco  18150  estrchom  18171  funcestrcsetclem5  18189  funcsetcestrclem5  18204  evlf2val  18264  curf11  18271  curf12  18272  curf2val  18275  uncfval  18279  diagval  18285  hof2  18302  yonval  18306  gsumval2a  18698  gsumval2  18699  mndpsuppss  18778  gsumwspan  18859  efmnd  18883  ghmqusnsglem1  19298  ghmqusnsglem2  19299  ghmqusnsg  19300  ghmquskerlem1  19301  ghmquskerco  19302  ghmquskerlem2  19303  ghmquskerlem3  19304  ghmqusker  19305  orbstafun  19329  orbstaval  19330  symgval  19388  psgnvalii  19527  lsmhash  19723  frgpupval  19792  qusabl  19883  gsumval3  19925  gsumreidx  19935  gsumzaddlem  19939  gsummptshft  19954  telgsumfzslem  20006  telgsumfz  20008  telgsumfz0  20010  dpjval  20076  prdsrngd  20173  srgbinomlem3  20225  srgbinomlem4  20226  mulgass3  20353  rngcval  20618  rnghmsscmap2  20629  rnghmsscmap  20630  funcrngcsetc  20640  ringcval  20647  rhmsscmap2  20658  rhmsscmap  20659  funcringcsetc  20674  srhmsubclem3  20679  srhmsubc  20680  fldhmsubc  20786  lcomfsupp  20900  rmodislmodlem  20927  rmodislmod  20928  sraval  21174  srasca  21183  srascaOLD  21184  crngridl  21290  quscrng  21293  rhmqusnsg  21295  pzriprnglem11  21502  znval  21550  znzrhfo  21566  znunithash  21583  cygznlem2  21587  frobrhm  21594  pjfval  21726  pjpm  21728  frlmgsum  21792  frlmipval  21799  frlmphllem  21800  frlmphl  21801  frlmsslsp  21816  frlmup1  21818  gsumbagdiaglem  21950  psrass1lem  21952  rhmpsrlem1  21960  psrass1  21984  psrdi  21985  psrdir  21986  psrass23l  21987  psrascl  21999  mplval  22009  mplsubglem  22019  mplsubrglem  22024  mplmonmul  22054  mplcoe1  22055  opsrval  22064  psrbagev1  22101  psrbagev2  22102  evlslem6  22105  evlslem1  22106  evlsval  22110  mpfconst  22125  mpff  22128  mpfaddcl  22129  mpfmulcl  22130  mpfind  22131  mhpmulcl  22153  mhpaddcl  22155  psdcoef  22164  psdmplcl  22166  psdadd  22167  ply1lss  22198  gsumply1subr  22235  coe1add  22267  coe1tm  22276  coe1tmmul  22280  cply1mul  22300  ply1coe  22302  evl1expd  22349  pf1mpf  22356  pf1ind  22359  mhmcompl  22384  mhmcoaddmpl  22385  rhmmpl  22387  rhmply1vsca  22392  mamufv  22398  mamuass  22406  mamuvs1  22409  mamuvs2  22410  matgsum  22443  dmatmul  22503  scmatval  22510  scmatrhmval  22533  mvmulfv  22550  mavmulfv  22552  mavmulass  22555  marrepeval  22569  marepveval  22574  submaeval  22588  mdetrsca  22609  mdetunilem9  22626  mdetuni0  22627  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  smadiadetlem3  22674  cramerlem1  22693  mat2pmatmul  22737  m2cpminvid  22759  decpmatfsupp  22775  decpmatmullem  22777  decpmatmul  22778  decpmatmulsumfsupp  22779  pmatcollpw1lem1  22780  pmatcollpw3fi1lem1  22792  pmatcollpwscmatlem2  22796  pm2mpfval  22802  pm2mpf  22804  mply1topmatcllem  22809  mp2pm2mplem3  22814  mp2pm2mplem4  22815  pm2mpmhmlem1  22824  pm2mpmhmlem2  22825  pm2mp  22831  chfacfscmulfsupp  22865  chfacfscmulgsum  22866  chfacfpmmulfsupp  22869  chfacfpmmulgsum  22870  cpmidpmatlem3  22878  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  cayhamlem4  22894  xpstopnlem2  23819  fcfval  24041  tsmsxplem1  24161  tsmsxplem2  24162  tusval  24274  xpsdsfn  24387  xpsxmet  24390  xpsdsval  24391  xpsmet  24392  tmsval  24493  met1stc  24534  metuval  24562  cnmpopc  24955  pi1val  25070  pi1addf  25080  pi1addval  25081  pi1grplem  25082  rrxnm  25425  rrxcph  25426  rrxmval  25439  mbfmulc2  25698  mbfmul  25761  itg2mulclem  25781  ibladd  25856  itgadd  25860  itgabs  25870  bddmulibl  25874  dvmulf  25980  dvcmulf  25982  dvmptmul  25999  cmvth  26029  dvlip  26032  ftc1lem4  26080  mdegmullem  26117  coe1mul3  26138  r1pval  26197  plyco  26280  dgrcolem1  26313  elqaalem3  26363  taylpfval  26406  taylthlem2  26416  taylthlem2OLD  26417  pserdvlem2  26472  advlogexp  26697  logtayl  26702  logccv  26705  dvcxp1  26782  dvcncxp1  26785  logbmpt  26831  logbfval  26833  relogbf  26834  dvatan  26978  cxp2lim  27020  cxploglim2  27022  lgamgulmlem2  27073  lgamgulm2  27079  lgamcvglem  27083  lgamf  27085  basellem7  27130  basellem8  27131  basellem9  27132  fsumdvdscom  27228  logexprlim  27269  dchrfi  27299  gausslemma2dlem2  27411  gausslemma2dlem3  27412  2lgslem1b  27436  chtppilimlem2  27518  chebbnd2  27521  chto1lb  27522  chpchtlim  27523  chpo1ub  27524  vmadivsum  27526  dchrisum0lem3  27563  mudivsum  27574  logdivsum  27577  log2sumbnd  27588  selberglem1  27589  selberg2lem  27594  selberg2  27595  selbergr  27612  negsval  28057  wlkp1  29699  cyclnumvtx  29820  wwlksnextsurj  29920  wwlksnextbij  29922  clwlkclwwlklem2a1  30011  clwlkclwwlkf1  30029  eupth2eucrct  30236  frgrncvvdeq  30328  numclwlk2lem2fv  30397  numclwwlk2lem3  30399  ofoprabco  32674  fsuppcurry1  32736  fsuppcurry2  32737  offinsupp1  32738  ressprs  32954  resspos  32956  mntoval  32972  mgcoval  32976  mndlactf1  33031  mndlactfo  33032  mndractf1  33033  mndractfo  33034  mndlactf1o  33035  mndractf1o  33036  lmodvslmhm  33053  gsumwrd2dccat  33070  cycpmco2f1  33144  cycpmco2rn  33145  cycpmco2lem2  33147  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  archirngz  33196  archiabllem2a  33201  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnsubrunlem2  33252  rlocval  33263  fracval  33306  quslmod  33386  quslmhm  33387  quslvec  33388  qustriv  33392  qustrivr  33393  unitprodclb  33417  nsgmgc  33440  nsgqusf1olem1  33441  nsgqusf1olem2  33442  nsgqusf1olem3  33443  lmhmqusker  33445  rhmquskerlem  33453  elrspunidl  33456  qsidomlem1  33480  qsidomlem2  33481  opprqusbas  33516  opprqusplusg  33517  opprqusmulr  33519  opprqus1r  33520  qsdrngilem  33522  qsdrngi  33523  rprmdvdsprod  33562  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  1arithufdlem3  33574  dfufd2lem  33577  zringfrac  33582  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  ply1gsumz  33619  r1plmhm  33630  resssra  33638  ply1degltdimlem  33673  ply1degltdim  33674  qusdimsum  33679  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  lactlmhm  33685  fldgenfldext  33718  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  algextdeglem4  33761  algextdeglem6  33763  algextdeglem7  33764  submateq  33808  lmatcl  33815  mdetpmtr1  33822  madjusmdetlem1  33826  madjusmdetlem3  33828  qqhvval  33984  esumfzf  34070  esumpfinvallem  34075  esumpmono  34080  esummulc1  34082  esumcvg  34087  esumgect  34091  ofcval  34100  omssubadd  34302  sitgfval  34343  sitmcl  34353  sseqfv2  34396  cndprobval  34435  ballotlemfval  34492  ballotlemsv  34512  ballotlemsf1o  34516  ofcccat  34558  signsplypnf  34565  signsply0  34566  signstfval  34579  signshf  34603  reprpmtf1o  34641  reprdifc  34642  logdivsqrle  34665  hgt750lemg  34669  hgt750lema  34672  lpadval  34691  cvmliftlem8  35297  cvmliftphtlem  35322  fmla1  35392  gonarlem  35399  sategoelfvb  35424  mrsubval  35514  ellcsrspsn  35646  r1peuqusdeg1  35648  fwddifval  36163  knoppcnlem1  36494  knoppcnlem6  36499  unbdqndv2lem2  36511  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem19  37646  poimirlem22  37649  poimirlem23  37650  broucube  37661  dvtan  37677  itg2addnc  37681  ibladdnc  37684  itgaddnc  37687  itgmulc2nclem2  37694  itgmulc2nc  37695  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem3  37702  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  dvasin  37711  dvacos  37712  dvreasin  37713  dvreacos  37714  areacirclem1  37715  areacirc  37720  fsumshftd  38953  hlrelat5N  39403  rhmzrhval  41971  aks6d1c1  42117  hashscontpow  42123  aks6d1c4  42125  aks6d1c2lem3  42127  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5lem0  42136  aks6d1c5lem3  42138  aks6d1c5lem2  42139  aks6d1c5  42140  sticksstones3  42149  sticksstones8  42154  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem1  42171  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  aks6d1c6isolem3  42177  aks6d1c6lem5  42178  aks6d1c7lem2  42182  unitscyglem1  42196  readvrec2  42391  readvrec  42392  readvcot  42394  frlmfzolen  42513  frlmfzoccat  42515  frlmvscadiccat  42516  evlscl  42568  evlsval3  42569  evlsvval  42570  evlsvvval  42573  evlsbagval  42576  evlsexpval  42577  evlsaddval  42578  evlsmulval  42579  evlsevl  42581  evlcl  42582  evladdval  42585  evlmulval  42586  selvcl  42593  evlselv  42597  fsuppind  42600  mhpind  42604  mhphflem  42606  prjspner  42629  prjspnvs  42630  prjspnfv01  42634  prjspner01  42635  prjspner1  42636  0prjspnrel  42637  prjcrv0  42643  mzpclall  42738  mzpsubst  42759  eldioph2  42773  rabdiophlem2  42813  irrapxlem1  42833  mzpcong  42984  mendlmod  43201  naddcnff  43375  relexpmulnn  43722  iunrelexpuztr  43732  mnringvald  44227  mnringmulrvald  44246  radcnvrat  44333  hashnzfzclim  44341  lhe4.4ex1a  44348  expgrowthi  44352  expgrowth  44354  bccval  44357  binomcxplemrat  44369  binomcxplemfrat  44370  binomcxplemradcnv  44371  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  unirnmap  45213  unirnmapsn  45219  ssmapsn  45221  iocopn  45533  icoopn  45538  divcnvg  45642  sumnnodd  45645  climsubmpt  45675  dvsinax  45928  fperdvper  45934  dvdivf  45937  dvnprodlem1  45961  itgsincmulx  45989  stoweidlem59  46074  etransclem4  46253  etransclem13  46262  etransclem25  46274  etransclem48  46297  rrxtopnfi  46302  sge0tsms  46395  elhoi  46557  ovnval2  46560  ovnval2b  46567  ovncvrrp  46579  ovn0lem  46580  ovncl  46582  ovnome  46588  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvle  46615  ovnlecvr2  46625  ovncvr2  46626  ovnsubadd2lem  46660  ovnovollem1  46671  vonvolmbl  46676  iunhoiioolem  46690  vonioolem1  46695  vonioolem2  46696  vonicclem2  46699  smfresal  46803  smfres  46805  smfmullem4  46809  smfco  46817  adddmmbl  46848  muldmmbl  46850  fmtno  47516  isubgruhgr  47854  grtriprop  47908  grtriclwlk3  47912  gpgvtx  48002  gpgiedg  48003  intopval  48118  clintopval  48120  rngchomALTV  48184  funcringcsetcALTV2lem5  48210  ringchomALTV  48218  funcringcsetclem5ALTV  48233  srhmsubcALTVlem2  48240  srhmsubcALTV  48241  fldhmsubcALTV  48249  zlmodzxzscm  48273  zlmodzxzadd  48274  rmsupp0  48284  domnmsuppn0  48285  rmsuppss  48286  ply1mulgsumlem3  48305  ply1mulgsumlem4  48306  ply1mulgsum  48307  dmatALTval  48317  lincop  48325  lincval  48326  linc1  48342  lincresunit3lem1  48396  fdivmpt  48461  fdivmptfv  48466  refdivmptfv  48467  digval  48519  2arymptfv  48571  2arymaptfo  48575  itcovalpclem1  48591  itcovalt2lem1  48596  ackvalsuc1mpt  48599  ackval1  48602  ackval2  48603  ackval3  48604  ackval42  48617  line2xlem  48674  upfval2  48934  swapfval  48968  tposcurf1  48999  tposcurf2val  49001  fucofvalg  49013  fuco112x  49027  fuco23  49036  fucoid  49043  fucocolem4  49051