Theorem ovexd 7425

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  (class class class)co 7390

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  caofidlcan  7694  caofass  7696  caofdi  7698  caofdir  7699  caonncan  7700  suppofssd  8185  mapsnend  9010  snmapen  9012  pw2eng  9052  mapen  9111  mapxpen  9113  mapunen  9116  mapdom2  9118  cantnfcl  9627  cantnfle  9631  cantnflt  9632  cantnflt2  9633  cantnfp1lem2  9639  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1d  9648  cantnflem1  9649  cnfcomlem  9659  cnfcom  9660  cnfcom2lem  9661  cnfcom3lem  9663  fzen  13509  seqf1o  14015  wrdexg  14496  wrdnval  14517  pfxval  14645  pfxswrd  14678  splval  14723  cshwsexaOLD  14797  ofccat  14942  climshftlem  15547  climshft  15549  climshft2  15555  caucvgr  15649  fsumrev  15752  hashdvds  16752  setsabs  17156  ressress  17224  firest  17402  prdsvscafval  17450  qusval  17512  xpsbas  17542  xpsadd  17544  xpsmul  17545  xpssca  17546  xpsvsca  17547  xpsless  17548  xpsle  17549  homfval  17660  comfval  17668  cicfval  17766  rescabs  17802  rescabs2  17803  resscat  17821  funcres2c  17872  ressffth  17909  fucbas  17932  fuccoval  17935  setchom  18049  catchom  18072  catcco  18074  estrchom  18095  funcestrcsetclem5  18112  funcsetcestrclem5  18127  evlf2val  18187  curf11  18194  curf12  18195  curf2val  18198  uncfval  18202  diagval  18208  hof2  18225  yonval  18229  gsumval2a  18619  gsumval2  18620  mndpsuppss  18699  gsumwspan  18780  efmnd  18804  ghmqusnsglem1  19219  ghmqusnsglem2  19220  ghmqusnsg  19221  ghmquskerlem1  19222  ghmquskerco  19223  ghmquskerlem2  19224  ghmquskerlem3  19225  ghmqusker  19226  orbstafun  19250  orbstaval  19251  symgval  19308  psgnvalii  19446  lsmhash  19642  frgpupval  19711  qusabl  19802  gsumval3  19844  gsumreidx  19854  gsumzaddlem  19858  gsummptshft  19873  telgsumfzslem  19925  telgsumfz  19927  telgsumfz0  19929  dpjval  19995  prdsrngd  20092  srgbinomlem3  20144  srgbinomlem4  20145  mulgass3  20269  rngcval  20534  rnghmsscmap2  20545  rnghmsscmap  20546  funcrngcsetc  20556  ringcval  20563  rhmsscmap2  20574  rhmsscmap  20575  funcringcsetc  20590  srhmsubclem3  20595  srhmsubc  20596  fldhmsubc  20701  lcomfsupp  20815  rmodislmodlem  20842  rmodislmod  20843  sraval  21089  srasca  21094  crngridl  21197  quscrng  21200  rhmqusnsg  21202  pzriprnglem11  21408  znval  21452  znzrhfo  21464  znunithash  21481  cygznlem2  21485  frobrhm  21492  pjfval  21622  pjpm  21624  frlmgsum  21688  frlmipval  21695  frlmphllem  21696  frlmphl  21697  frlmsslsp  21712  frlmup1  21714  gsumbagdiaglem  21846  psrass1lem  21848  rhmpsrlem1  21856  psrass1  21880  psrdi  21881  psrdir  21882  psrass23l  21883  psrascl  21895  mplval  21905  mplsubglem  21915  mplsubrglem  21920  mplmonmul  21950  mplcoe1  21951  opsrval  21960  psrbagev1  21991  psrbagev2  21992  evlslem6  21995  evlslem1  21996  evlsval  22000  mpfconst  22015  mpff  22018  mpfaddcl  22019  mpfmulcl  22020  mpfind  22021  mhpmulcl  22043  mhpaddcl  22045  psdcoef  22054  psdmplcl  22056  psdadd  22057  ply1lss  22088  gsumply1subr  22125  coe1add  22157  coe1tm  22166  coe1tmmul  22170  cply1mul  22190  ply1coe  22192  evl1expd  22239  pf1mpf  22246  pf1ind  22249  mhmcompl  22274  mhmcoaddmpl  22275  rhmmpl  22277  rhmply1vsca  22282  mamufv  22288  mamuass  22296  mamuvs1  22299  mamuvs2  22300  matgsum  22331  dmatmul  22391  scmatval  22398  scmatrhmval  22421  mvmulfv  22438  mavmulfv  22440  mavmulass  22443  marrepeval  22457  marepveval  22462  submaeval  22476  mdetrsca  22497  mdetunilem9  22514  mdetuni0  22515  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  smadiadetlem3  22562  cramerlem1  22581  mat2pmatmul  22625  m2cpminvid  22647  decpmatfsupp  22663  decpmatmullem  22665  decpmatmul  22666  decpmatmulsumfsupp  22667  pmatcollpw1lem1  22668  pmatcollpw3fi1lem1  22680  pmatcollpwscmatlem2  22684  pm2mpfval  22690  pm2mpf  22692  mply1topmatcllem  22697  mp2pm2mplem3  22702  mp2pm2mplem4  22703  pm2mpmhmlem1  22712  pm2mpmhmlem2  22713  pm2mp  22719  chfacfscmulfsupp  22753  chfacfscmulgsum  22754  chfacfpmmulfsupp  22757  chfacfpmmulgsum  22758  cpmidpmatlem3  22766  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  cayhamlem4  22782  xpstopnlem2  23705  fcfval  23927  tsmsxplem1  24047  tsmsxplem2  24048  tusval  24160  xpsdsfn  24272  xpsxmet  24275  xpsdsval  24276  xpsmet  24277  tmsval  24376  met1stc  24416  metuval  24444  cnmpopc  24829  pi1val  24944  pi1addf  24954  pi1addval  24955  pi1grplem  24956  rrxnm  25298  rrxcph  25299  rrxmval  25312  mbfmulc2  25571  mbfmul  25634  itg2mulclem  25654  ibladd  25729  itgadd  25733  itgabs  25743  bddmulibl  25747  dvmulf  25853  dvcmulf  25855  dvmptmul  25872  cmvth  25902  dvlip  25905  ftc1lem4  25953  mdegmullem  25990  coe1mul3  26011  r1pval  26070  plyco  26153  dgrcolem1  26186  elqaalem3  26236  taylpfval  26279  taylthlem2  26289  taylthlem2OLD  26290  pserdvlem2  26345  advlogexp  26571  logtayl  26576  logccv  26579  dvcxp1  26656  dvcncxp1  26659  logbmpt  26705  logbfval  26707  relogbf  26708  dvatan  26852  cxp2lim  26894  cxploglim2  26896  lgamgulmlem2  26947  lgamgulm2  26953  lgamcvglem  26957  lgamf  26959  basellem7  27004  basellem8  27005  basellem9  27006  fsumdvdscom  27102  logexprlim  27143  dchrfi  27173  gausslemma2dlem2  27285  gausslemma2dlem3  27286  2lgslem1b  27310  chtppilimlem2  27392  chebbnd2  27395  chto1lb  27396  chpchtlim  27397  chpo1ub  27398  vmadivsum  27400  dchrisum0lem3  27437  mudivsum  27448  logdivsum  27451  log2sumbnd  27462  selberglem1  27463  selberg2lem  27468  selberg2  27469  selbergr  27486  negsval  27938  wlkp1  29616  cyclnumvtx  29737  wwlksnextsurj  29837  wwlksnextbij  29839  clwlkclwwlklem2a1  29928  clwlkclwwlkf1  29946  eupth2eucrct  30153  frgrncvvdeq  30245  numclwlk2lem2fv  30314  numclwwlk2lem3  30316  ofoprabco  32595  fsuppcurry1  32655  fsuppcurry2  32656  offinsupp1  32657  ressprs  32897  resspos  32899  mntoval  32915  mgcoval  32919  mndlactf1  32974  mndlactfo  32975  mndractf1  32976  mndractfo  32977  mndlactf1o  32978  mndractf1o  32979  lmodvslmhm  32997  gsumwrd2dccat  33014  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2  33097  conjga  33134  cntrval2  33135  fxpsubm  33136  archirngz  33150  archiabllem2a  33155  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnsubrunlem2  33206  rlocval  33217  fracval  33261  quslmod  33336  quslmhm  33337  quslvec  33338  qustriv  33342  qustrivr  33343  unitprodclb  33367  nsgmgc  33390  nsgqusf1olem1  33391  nsgqusf1olem2  33392  nsgqusf1olem3  33393  lmhmqusker  33395  rhmquskerlem  33403  elrspunidl  33406  qsidomlem1  33430  qsidomlem2  33431  opprqusbas  33466  opprqusplusg  33467  opprqusmulr  33469  opprqus1r  33470  qsdrngilem  33472  qsdrngi  33473  rprmdvdsprod  33512  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  1arithufdlem3  33524  dfufd2lem  33527  zringfrac  33532  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1gsumz  33571  r1plmhm  33582  resssra  33590  ply1degltdimlem  33625  ply1degltdim  33626  qusdimsum  33631  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  lactlmhm  33637  fldgenfldext  33670  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  algextdeglem4  33717  algextdeglem6  33719  algextdeglem7  33720  submateq  33806  lmatcl  33813  mdetpmtr1  33820  madjusmdetlem1  33824  madjusmdetlem3  33826  qqhvval  33980  esumfzf  34066  esumpfinvallem  34071  esumpmono  34076  esummulc1  34078  esumcvg  34083  esumgect  34087  ofcval  34096  omssubadd  34298  sitgfval  34339  sitmcl  34349  sseqfv2  34392  cndprobval  34431  ballotlemfval  34488  ballotlemsv  34508  ballotlemsf1o  34512  ofcccat  34541  signsplypnf  34548  signsply0  34549  signstfval  34562  signshf  34586  reprpmtf1o  34624  reprdifc  34625  logdivsqrle  34648  hgt750lemg  34652  hgt750lema  34655  lpadval  34674  cvmliftlem8  35286  cvmliftphtlem  35311  fmla1  35381  gonarlem  35388  sategoelfvb  35413  mrsubval  35503  ellcsrspsn  35635  r1peuqusdeg1  35637  fwddifval  36157  knoppcnlem1  36488  knoppcnlem6  36493  unbdqndv2lem2  36505  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem19  37640  poimirlem22  37643  poimirlem23  37644  broucube  37655  dvtan  37671  itg2addnc  37675  ibladdnc  37678  itgaddnc  37681  itgmulc2nclem2  37688  itgmulc2nc  37689  itgabsnc  37690  ftc1cnnclem  37692  ftc1anclem3  37696  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  dvasin  37705  dvacos  37706  dvreasin  37707  dvreacos  37708  areacirclem1  37709  areacirc  37714  fsumshftd  38952  hlrelat5N  39402  rhmzrhval  41966  aks6d1c1  42111  hashscontpow  42117  aks6d1c4  42119  aks6d1c2lem3  42121  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5lem0  42130  aks6d1c5lem3  42132  aks6d1c5lem2  42133  aks6d1c5  42134  sticksstones3  42143  sticksstones8  42148  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem1  42165  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  aks6d1c6isolem3  42171  aks6d1c6lem5  42172  aks6d1c7lem2  42176  unitscyglem1  42190  readvrec2  42356  readvrec  42357  readvcot  42359  frlmfzolen  42498  frlmfzoccat  42500  frlmvscadiccat  42501  evlscl  42553  evlsval3  42554  evlsvval  42555  evlsvvval  42558  evlsbagval  42561  evlsexpval  42562  evlsaddval  42563  evlsmulval  42564  evlsevl  42566  evlcl  42567  evladdval  42570  evlmulval  42571  selvcl  42578  evlselv  42582  fsuppind  42585  mhpind  42589  mhphflem  42591  prjspner  42614  prjspnvs  42615  prjspnfv01  42619  prjspner01  42620  prjspner1  42621  0prjspnrel  42622  prjcrv0  42628  mzpclall  42722  mzpsubst  42743  eldioph2  42757  rabdiophlem2  42797  irrapxlem1  42817  mzpcong  42968  mendlmod  43185  naddcnff  43358  relexpmulnn  43705  iunrelexpuztr  43715  mnringvald  44209  mnringmulrvald  44223  radcnvrat  44310  hashnzfzclim  44318  lhe4.4ex1a  44325  expgrowthi  44329  expgrowth  44331  bccval  44334  binomcxplemrat  44346  binomcxplemfrat  44347  binomcxplemradcnv  44348  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  unirnmap  45209  unirnmapsn  45215  ssmapsn  45217  iocopn  45525  icoopn  45530  divcnvg  45632  sumnnodd  45635  climsubmpt  45665  dvsinax  45918  fperdvper  45924  dvdivf  45927  dvnprodlem1  45951  itgsincmulx  45979  stoweidlem59  46064  etransclem4  46243  etransclem13  46252  etransclem25  46264  etransclem48  46287  rrxtopnfi  46292  sge0tsms  46385  elhoi  46547  ovnval2  46550  ovnval2b  46557  ovncvrrp  46569  ovn0lem  46570  ovncl  46572  ovnome  46578  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvle  46605  ovnlecvr2  46615  ovncvr2  46616  ovnsubadd2lem  46650  ovnovollem1  46661  vonvolmbl  46666  iunhoiioolem  46680  vonioolem1  46685  vonioolem2  46686  vonicclem2  46689  smfresal  46793  smfres  46795  smfmullem4  46799  smfco  46807  adddmmbl  46838  muldmmbl  46840  fmtno  47534  isubgruhgr  47872  grtriprop  47944  grtriclwlk3  47948  gpgvtx  48038  gpgiedg  48039  intopval  48194  clintopval  48196  rngchomALTV  48260  funcringcsetcALTV2lem5  48286  ringchomALTV  48294  funcringcsetclem5ALTV  48309  srhmsubcALTVlem2  48316  srhmsubcALTV  48317  fldhmsubcALTV  48325  zlmodzxzscm  48349  zlmodzxzadd  48350  rmsupp0  48360  domnmsuppn0  48361  rmsuppss  48362  ply1mulgsumlem3  48381  ply1mulgsumlem4  48382  ply1mulgsum  48383  dmatALTval  48393  lincop  48401  lincval  48402  linc1  48418  lincresunit3lem1  48472  fdivmpt  48533  fdivmptfv  48538  refdivmptfv  48539  digval  48591  2arymptfv  48643  2arymaptfo  48647  itcovalpclem1  48663  itcovalt2lem1  48668  ackvalsuc1mpt  48671  ackval1  48674  ackval2  48675  ackval3  48676  ackval42  48689  line2xlem  48746  upfval2  49170  swapfval  49255  tposcurf1  49292  tposcurf2val  49294  fucofvalg  49311  fuco112x  49325  fuco23  49334  fucoid  49341  fucocolem4  49349  prcofvalg  49369  prcof1  49381  opf2fval  49398  lanval  49612  ranval  49613