Theorem ovexd 7402

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429  (class class class)co 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-sn 4568  df-pr 4570  df-uni 4851  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  caofidlcan  7669  caofass  7671  caofdi  7673  caofdir  7674  caonncan  7675  suppofssd  8153  mapsnend  8983  snmapen  8985  pw2eng  9021  mapen  9079  mapxpen  9081  mapunen  9084  mapdom2  9086  cantnfcl  9588  cantnfle  9592  cantnflt  9593  cantnflt2  9594  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom3lem  9624  fzen  13495  seqf1o  14005  wrdexg  14486  wrdnval  14507  pfxval  14636  pfxswrd  14668  splval  14713  ofccat  14931  climshftlem  15536  climshft  15538  climshft2  15544  caucvgr  15638  fsumrev  15741  hashdvds  16745  setsabs  17149  ressress  17217  firest  17395  prdsvscafval  17443  qusval  17506  xpsbas  17536  xpsadd  17538  xpsmul  17539  xpssca  17540  xpsvsca  17541  xpsless  17542  xpsle  17543  homfval  17658  comfval  17666  cicfval  17764  rescabs  17800  rescabs2  17801  resscat  17819  funcres2c  17870  ressffth  17907  fucbas  17930  fuccoval  17933  setchom  18047  catchom  18070  catcco  18072  estrchom  18093  funcestrcsetclem5  18110  funcsetcestrclem5  18125  evlf2val  18185  curf11  18192  curf12  18193  curf2val  18196  uncfval  18200  diagval  18206  hof2  18223  yonval  18227  resspos  18395  gsumval2a  18653  gsumval2  18654  mndpsuppss  18733  gsumwspan  18814  efmnd  18838  ghmqusnsglem1  19255  ghmqusnsglem2  19256  ghmqusnsg  19257  ghmquskerlem1  19258  ghmquskerco  19259  ghmquskerlem2  19260  ghmquskerlem3  19261  ghmqusker  19262  orbstafun  19286  orbstaval  19287  symgval  19346  psgnvalii  19484  lsmhash  19680  frgpupval  19749  qusabl  19840  gsumval3  19882  gsumreidx  19892  gsumzaddlem  19896  gsummptshft  19911  telgsumfzslem  19963  telgsumfz  19965  telgsumfz0  19967  dpjval  20033  prdsrngd  20157  srgbinomlem3  20209  srgbinomlem4  20210  mulgass3  20333  rngcval  20595  rnghmsscmap2  20606  rnghmsscmap  20607  funcrngcsetc  20617  ringcval  20624  rhmsscmap2  20635  rhmsscmap  20636  funcringcsetc  20651  srhmsubclem3  20656  srhmsubc  20657  fldhmsubc  20762  lcomfsupp  20897  rmodislmodlem  20924  rmodislmod  20925  sraval  21170  srasca  21175  crngridl  21278  quscrng  21281  rhmqusnsg  21283  pzriprnglem11  21471  znval  21515  znzrhfo  21527  znunithash  21544  cygznlem2  21548  frobrhm  21555  pjfval  21686  pjpm  21688  frlmgsum  21752  frlmipval  21759  frlmphllem  21760  frlmphl  21761  frlmsslsp  21776  frlmup1  21778  gsumbagdiaglem  21910  psrass1lem  21912  rhmpsrlem1  21919  psrass1  21942  psrdi  21943  psrdir  21944  psrass23l  21945  psrascl  21957  mplval  21967  mplsubglem  21977  mplsubrglem  21982  mplmonmul  22014  mplcoe1  22015  opsrval  22024  psrbagev1  22055  psrbagev2  22056  evlslem6  22059  evlslem1  22060  evlsval  22064  evlsval3  22067  evlsvval  22068  evlsvvval  22071  evlcl  22080  evladdval  22081  evlmulval  22082  mpfconst  22087  mpff  22090  mpfaddcl  22091  mpfmulcl  22092  mpfind  22093  mhpmulcl  22115  mhpaddcl  22117  psdcoef  22126  psdmplcl  22128  psdadd  22129  ply1lss  22160  gsumply1subr  22197  coe1add  22229  coe1tm  22238  coe1tmmul  22242  cply1mul  22261  ply1coe  22263  evl1expd  22310  pf1mpf  22317  pf1ind  22320  mhmcompl  22345  mhmcoaddmpl  22346  rhmmpl  22348  rhmply1vsca  22353  mamufv  22359  mamuass  22367  mamuvs1  22370  mamuvs2  22371  matgsum  22402  dmatmul  22462  scmatval  22469  scmatrhmval  22492  mvmulfv  22509  mavmulfv  22511  mavmulass  22514  marrepeval  22528  marepveval  22533  submaeval  22547  mdetrsca  22568  mdetunilem9  22585  mdetuni0  22586  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  smadiadetlem3  22633  cramerlem1  22652  mat2pmatmul  22696  m2cpminvid  22718  decpmatfsupp  22734  decpmatmullem  22736  decpmatmul  22737  decpmatmulsumfsupp  22738  pmatcollpw1lem1  22739  pmatcollpw3fi1lem1  22751  pmatcollpwscmatlem2  22755  pm2mpfval  22761  pm2mpf  22763  mply1topmatcllem  22768  mp2pm2mplem3  22773  mp2pm2mplem4  22774  pm2mpmhmlem1  22783  pm2mpmhmlem2  22784  pm2mp  22790  chfacfscmulfsupp  22824  chfacfscmulgsum  22825  chfacfpmmulfsupp  22828  chfacfpmmulgsum  22829  cpmidpmatlem3  22837  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cayhamlem4  22853  xpstopnlem2  23776  fcfval  23998  tsmsxplem1  24118  tsmsxplem2  24119  tusval  24230  xpsdsfn  24342  xpsxmet  24345  xpsdsval  24346  xpsmet  24347  tmsval  24446  met1stc  24486  metuval  24514  cnmpopc  24895  pi1val  25004  pi1addf  25014  pi1addval  25015  pi1grplem  25016  rrxnm  25358  rrxcph  25359  rrxmval  25372  mbfmulc2  25630  mbfmul  25693  itg2mulclem  25713  ibladd  25788  itgadd  25792  itgabs  25802  bddmulibl  25806  dvmulf  25910  dvcmulf  25912  dvmptmul  25928  cmvth  25958  dvlip  25960  ftc1lem4  26006  mdegmullem  26043  coe1mul3  26064  r1pval  26123  plyco  26206  dgrcolem1  26238  elqaalem3  26287  taylpfval  26330  taylthlem2  26339  pserdvlem2  26393  advlogexp  26619  logtayl  26624  logccv  26627  dvcxp1  26704  dvcncxp1  26707  logbmpt  26752  logbfval  26754  relogbf  26755  dvatan  26899  cxp2lim  26940  cxploglim2  26942  lgamgulmlem2  26993  lgamgulm2  26999  lgamcvglem  27003  lgamf  27005  basellem7  27050  basellem8  27051  basellem9  27052  fsumdvdscom  27148  logexprlim  27188  dchrfi  27218  gausslemma2dlem2  27330  gausslemma2dlem3  27331  2lgslem1b  27355  chtppilimlem2  27437  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  vmadivsum  27445  dchrisum0lem3  27482  mudivsum  27493  logdivsum  27496  log2sumbnd  27507  selberglem1  27508  selberg2lem  27513  selberg2  27514  selbergr  27531  negsval  28017  wlkp1  29748  cyclnumvtx  29868  wwlksnextsurj  29968  wwlksnextbij  29970  clwlkclwwlklem2a1  30062  clwlkclwwlkf1  30080  eupth2eucrct  30287  frgrncvvdeq  30379  numclwlk2lem2fv  30448  numclwwlk2lem3  30450  ofoprabco  32737  fsuppcurry1  32797  fsuppcurry2  32798  offinsupp1  32799  ressprs  33026  mntoval  33042  mgcoval  33046  mndlactf1  33086  mndlactfo  33087  mndractf1  33088  mndractfo  33089  mndlactf1o  33090  mndractf1o  33091  lmodvslmhm  33111  gsummulsubdishift2  33130  gsumwrd2dccat  33139  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  conjga  33231  cntrval2  33232  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  fxpsdrg  33236  archirngz  33250  archiabllem2a  33255  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnsubrunlem2  33309  rlocval  33320  fracval  33365  quslmod  33418  quslmhm  33419  quslvec  33420  qustriv  33424  qustrivr  33425  unitprodclb  33449  nsgmgc  33472  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475  lmhmqusker  33477  rhmquskerlem  33485  elrspunidl  33488  qsidomlem1  33512  qsidomlem2  33513  opprqusbas  33548  opprqusplusg  33549  opprqusmulr  33551  opprqus1r  33552  qsdrngilem  33554  qsdrngi  33555  rprmdvdsprod  33594  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  1arithufdlem3  33606  dfufd2lem  33609  zringfrac  33614  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ply1gsumz  33659  r1plmhm  33670  mplvrpmrhm  33691  psrgsum  33692  psrmonmul  33694  psrmonprod  33696  mplgsum  33697  splyval  33703  esplyfval1  33717  esplyfvaln  33718  vietadeg1  33722  resssra  33731  ply1degltdimlem  33766  ply1degltdim  33767  qusdimsum  33772  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  lactlmhm  33778  fldgenfldext  33812  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  extdgfialglem1  33836  extdgfialglem2  33837  extdgfialg  33838  algextdeglem4  33864  algextdeglem6  33866  algextdeglem7  33867  submateq  33953  lmatcl  33960  mdetpmtr1  33967  madjusmdetlem1  33971  madjusmdetlem3  33973  qqhvval  34127  esumfzf  34213  esumpfinvallem  34218  esumpmono  34223  esummulc1  34225  esumcvg  34230  esumgect  34234  ofcval  34243  omssubadd  34444  sitgfval  34485  sitmcl  34495  sseqfv2  34538  cndprobval  34577  ballotlemfval  34634  ballotlemsv  34654  ballotlemsf1o  34658  ofcccat  34687  signsplypnf  34694  signsply0  34695  signstfval  34708  signshf  34732  reprpmtf1o  34770  reprdifc  34771  logdivsqrle  34794  hgt750lemg  34798  hgt750lema  34801  lpadval  34820  cvmliftlem8  35474  cvmliftphtlem  35499  fmla1  35569  gonarlem  35576  sategoelfvb  35601  mrsubval  35691  ellcsrspsn  35823  r1peuqusdeg1  35825  fwddifval  36344  knoppcnlem1  36753  knoppcnlem6  36758  unbdqndv2lem2  36770  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem19  37960  poimirlem22  37963  poimirlem23  37964  broucube  37975  dvtan  37991  itg2addnc  37995  ibladdnc  37998  itgaddnc  38001  itgmulc2nclem2  38008  itgmulc2nc  38009  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem3  38016  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  dvasin  38025  dvacos  38026  dvreasin  38027  dvreacos  38028  areacirclem1  38029  areacirc  38034  fsumshftd  39398  hlrelat5N  39847  rhmzrhval  42411  aks6d1c1  42555  hashscontpow  42561  aks6d1c4  42563  aks6d1c2lem3  42565  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem0  42574  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks6d1c5  42578  sticksstones3  42587  sticksstones8  42592  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem1  42609  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6isolem3  42615  aks6d1c6lem5  42616  aks6d1c7lem2  42620  unitscyglem1  42634  readvrec2  42793  readvrec  42794  readvcot  42796  frlmfzolen  42948  frlmfzoccat  42950  frlmvscadiccat  42951  evlscl  42999  evlsbagval  43002  evlsexpval  43003  evlsaddval  43004  evlsmulval  43005  evlsevl  43007  selvcl  43016  evlselv  43020  fsuppind  43023  mhpind  43027  mhphflem  43029  prjspner  43052  prjspnvs  43053  prjspnfv01  43057  prjspner01  43058  prjspner1  43059  0prjspnrel  43060  prjcrv0  43066  mzpclall  43159  mzpsubst  43180  eldioph2  43194  rabdiophlem2  43230  irrapxlem1  43250  mzpcong  43400  mendlmod  43617  naddcnff  43790  relexpmulnn  44136  iunrelexpuztr  44146  mnringvald  44640  mnringmulrvald  44654  radcnvrat  44741  hashnzfzclim  44749  lhe4.4ex1a  44756  expgrowthi  44760  expgrowth  44762  bccval  44765  binomcxplemrat  44777  binomcxplemfrat  44778  binomcxplemradcnv  44779  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  unirnmap  45637  unirnmapsn  45643  ssmapsn  45645  iocopn  45950  icoopn  45955  divcnvg  46057  sumnnodd  46060  climsubmpt  46088  dvsinax  46341  fperdvper  46347  dvdivf  46350  dvnprodlem1  46374  itgsincmulx  46402  stoweidlem59  46487  etransclem4  46666  etransclem13  46675  etransclem25  46687  etransclem48  46710  rrxtopnfi  46715  sge0tsms  46808  elhoi  46970  ovnval2  46973  ovnval2b  46980  ovncvrrp  46992  ovn0lem  46993  ovncl  46995  ovnome  47001  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvle  47028  ovnlecvr2  47038  ovncvr2  47039  ovnsubadd2lem  47073  ovnovollem1  47084  vonvolmbl  47089  iunhoiioolem  47103  vonioolem1  47108  vonioolem2  47109  vonicclem2  47112  smfresal  47216  smfres  47218  smfmullem4  47222  smfco  47230  adddmmbl  47261  muldmmbl  47263  chnsuslle  47311  nthrucw  47316  sinnpoly  47339  fmtno  47992  isubgruhgr  48344  grtriprop  48417  grtriclwlk3  48421  gpgvtx  48519  gpgiedg  48520  intopval  48678  clintopval  48680  rngchomALTV  48744  funcringcsetcALTV2lem5  48770  ringchomALTV  48778  funcringcsetclem5ALTV  48793  srhmsubcALTVlem2  48800  srhmsubcALTV  48801  fldhmsubcALTV  48809  zlmodzxzscm  48833  zlmodzxzadd  48834  rmsupp0  48844  domnmsuppn0  48845  rmsuppss  48846  ply1mulgsumlem3  48864  ply1mulgsumlem4  48865  ply1mulgsum  48866  dmatALTval  48876  lincop  48884  lincval  48885  linc1  48901  lincresunit3lem1  48955  fdivmpt  49016  fdivmptfv  49021  refdivmptfv  49022  digval  49074  2arymptfv  49126  2arymaptfo  49130  itcovalpclem1  49146  itcovalt2lem1  49151  ackvalsuc1mpt  49154  ackval1  49157  ackval2  49158  ackval3  49159  ackval42  49172  line2xlem  49229  upfval2  49652  swapfval  49737  tposcurf1  49774  tposcurf2val  49776  fucofvalg  49793  fuco112x  49807  fuco23  49816  fucoid  49823  fucocolem4  49831  prcofvalg  49851  prcof1  49863  opf2fval  49880  lanval  50094  ranval  50095