Theorem ovexd 7404

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444  (class class class)co 7369

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 2701  ax-nul 5256

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-sn 4586  df-pr 4588  df-uni 4868  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  caofidlcan  7671  caofass  7673  caofdi  7675  caofdir  7676  caonncan  7677  suppofssd  8159  mapsnend  8984  snmapen  8986  pw2eng  9024  mapen  9082  mapxpen  9084  mapunen  9087  mapdom2  9089  cantnfcl  9596  cantnfle  9600  cantnflt  9601  cantnflt2  9602  cantnfp1lem2  9608  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1d  9617  cantnflem1  9618  cnfcomlem  9628  cnfcom  9629  cnfcom2lem  9630  cnfcom3lem  9632  fzen  13478  seqf1o  13984  wrdexg  14465  wrdnval  14486  pfxval  14614  pfxswrd  14647  splval  14692  cshwsexaOLD  14766  ofccat  14911  climshftlem  15516  climshft  15518  climshft2  15524  caucvgr  15618  fsumrev  15721  hashdvds  16721  setsabs  17125  ressress  17193  firest  17371  prdsvscafval  17419  qusval  17481  xpsbas  17511  xpsadd  17513  xpsmul  17514  xpssca  17515  xpsvsca  17516  xpsless  17517  xpsle  17518  homfval  17633  comfval  17641  cicfval  17739  rescabs  17775  rescabs2  17776  resscat  17794  funcres2c  17845  ressffth  17882  fucbas  17905  fuccoval  17908  setchom  18022  catchom  18045  catcco  18047  estrchom  18068  funcestrcsetclem5  18085  funcsetcestrclem5  18100  evlf2val  18160  curf11  18167  curf12  18168  curf2val  18171  uncfval  18175  diagval  18181  hof2  18198  yonval  18202  resspos  18370  gsumval2a  18594  gsumval2  18595  mndpsuppss  18674  gsumwspan  18755  efmnd  18779  ghmqusnsglem1  19194  ghmqusnsglem2  19195  ghmqusnsg  19196  ghmquskerlem1  19197  ghmquskerco  19198  ghmquskerlem2  19199  ghmquskerlem3  19200  ghmqusker  19201  orbstafun  19225  orbstaval  19226  symgval  19285  psgnvalii  19423  lsmhash  19619  frgpupval  19688  qusabl  19779  gsumval3  19821  gsumreidx  19831  gsumzaddlem  19835  gsummptshft  19850  telgsumfzslem  19902  telgsumfz  19904  telgsumfz0  19906  dpjval  19972  prdsrngd  20096  srgbinomlem3  20148  srgbinomlem4  20149  mulgass3  20273  rngcval  20538  rnghmsscmap2  20549  rnghmsscmap  20550  funcrngcsetc  20560  ringcval  20567  rhmsscmap2  20578  rhmsscmap  20579  funcringcsetc  20594  srhmsubclem3  20599  srhmsubc  20600  fldhmsubc  20705  lcomfsupp  20840  rmodislmodlem  20867  rmodislmod  20868  sraval  21114  srasca  21119  crngridl  21222  quscrng  21225  rhmqusnsg  21227  pzriprnglem11  21433  znval  21477  znzrhfo  21489  znunithash  21506  cygznlem2  21510  frobrhm  21517  pjfval  21648  pjpm  21650  frlmgsum  21714  frlmipval  21721  frlmphllem  21722  frlmphl  21723  frlmsslsp  21738  frlmup1  21740  gsumbagdiaglem  21872  psrass1lem  21874  rhmpsrlem1  21882  psrass1  21906  psrdi  21907  psrdir  21908  psrass23l  21909  psrascl  21921  mplval  21931  mplsubglem  21941  mplsubrglem  21946  mplmonmul  21976  mplcoe1  21977  opsrval  21986  psrbagev1  22017  psrbagev2  22018  evlslem6  22021  evlslem1  22022  evlsval  22026  mpfconst  22041  mpff  22044  mpfaddcl  22045  mpfmulcl  22046  mpfind  22047  mhpmulcl  22069  mhpaddcl  22071  psdcoef  22080  psdmplcl  22082  psdadd  22083  ply1lss  22114  gsumply1subr  22151  coe1add  22183  coe1tm  22192  coe1tmmul  22196  cply1mul  22216  ply1coe  22218  evl1expd  22265  pf1mpf  22272  pf1ind  22275  mhmcompl  22300  mhmcoaddmpl  22301  rhmmpl  22303  rhmply1vsca  22308  mamufv  22314  mamuass  22322  mamuvs1  22325  mamuvs2  22326  matgsum  22357  dmatmul  22417  scmatval  22424  scmatrhmval  22447  mvmulfv  22464  mavmulfv  22466  mavmulass  22469  marrepeval  22483  marepveval  22488  submaeval  22502  mdetrsca  22523  mdetunilem9  22540  mdetuni0  22541  gsummatr01lem3  22577  gsummatr01lem4  22578  gsummatr01  22579  smadiadetlem3  22588  cramerlem1  22607  mat2pmatmul  22651  m2cpminvid  22673  decpmatfsupp  22689  decpmatmullem  22691  decpmatmul  22692  decpmatmulsumfsupp  22693  pmatcollpw1lem1  22694  pmatcollpw3fi1lem1  22706  pmatcollpwscmatlem2  22710  pm2mpfval  22716  pm2mpf  22718  mply1topmatcllem  22723  mp2pm2mplem3  22728  mp2pm2mplem4  22729  pm2mpmhmlem1  22738  pm2mpmhmlem2  22739  pm2mp  22745  chfacfscmulfsupp  22779  chfacfscmulgsum  22780  chfacfpmmulfsupp  22783  chfacfpmmulgsum  22784  cpmidpmatlem3  22792  cpmadugsumlemB  22794  cpmadugsumlemC  22795  cpmadugsumlemF  22796  cayhamlem4  22808  xpstopnlem2  23731  fcfval  23953  tsmsxplem1  24073  tsmsxplem2  24074  tusval  24186  xpsdsfn  24298  xpsxmet  24301  xpsdsval  24302  xpsmet  24303  tmsval  24402  met1stc  24442  metuval  24470  cnmpopc  24855  pi1val  24970  pi1addf  24980  pi1addval  24981  pi1grplem  24982  rrxnm  25324  rrxcph  25325  rrxmval  25338  mbfmulc2  25597  mbfmul  25660  itg2mulclem  25680  ibladd  25755  itgadd  25759  itgabs  25769  bddmulibl  25773  dvmulf  25879  dvcmulf  25881  dvmptmul  25898  cmvth  25928  dvlip  25931  ftc1lem4  25979  mdegmullem  26016  coe1mul3  26037  r1pval  26096  plyco  26179  dgrcolem1  26212  elqaalem3  26262  taylpfval  26305  taylthlem2  26315  taylthlem2OLD  26316  pserdvlem2  26371  advlogexp  26597  logtayl  26602  logccv  26605  dvcxp1  26682  dvcncxp1  26685  logbmpt  26731  logbfval  26733  relogbf  26734  dvatan  26878  cxp2lim  26920  cxploglim2  26922  lgamgulmlem2  26973  lgamgulm2  26979  lgamcvglem  26983  lgamf  26985  basellem7  27030  basellem8  27031  basellem9  27032  fsumdvdscom  27128  logexprlim  27169  dchrfi  27199  gausslemma2dlem2  27311  gausslemma2dlem3  27312  2lgslem1b  27336  chtppilimlem2  27418  chebbnd2  27421  chto1lb  27422  chpchtlim  27423  chpo1ub  27424  vmadivsum  27426  dchrisum0lem3  27463  mudivsum  27474  logdivsum  27477  log2sumbnd  27488  selberglem1  27489  selberg2lem  27494  selberg2  27495  selbergr  27512  negsval  27971  wlkp1  29660  cyclnumvtx  29780  wwlksnextsurj  29880  wwlksnextbij  29882  clwlkclwwlklem2a1  29971  clwlkclwwlkf1  29989  eupth2eucrct  30196  frgrncvvdeq  30288  numclwlk2lem2fv  30357  numclwwlk2lem3  30359  ofoprabco  32638  fsuppcurry1  32698  fsuppcurry2  32699  offinsupp1  32700  ressprs  32938  mntoval  32954  mgcoval  32958  mndlactf1  33010  mndlactfo  33011  mndractf1  33012  mndractfo  33013  mndlactf1o  33014  mndractf1o  33015  lmodvslmhm  33033  gsumwrd2dccat  33050  cycpmco2f1  33096  cycpmco2rn  33097  cycpmco2lem2  33099  cycpmco2lem3  33100  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cycpmco2  33105  conjga  33142  cntrval2  33143  fxpsubm  33144  archirngz  33158  archiabllem2a  33163  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnsubrunlem2  33215  rlocval  33226  fracval  33270  quslmod  33322  quslmhm  33323  quslvec  33324  qustriv  33328  qustrivr  33329  unitprodclb  33353  nsgmgc  33376  nsgqusf1olem1  33377  nsgqusf1olem2  33378  nsgqusf1olem3  33379  lmhmqusker  33381  rhmquskerlem  33389  elrspunidl  33392  qsidomlem1  33416  qsidomlem2  33417  opprqusbas  33452  opprqusplusg  33453  opprqusmulr  33455  opprqus1r  33456  qsdrngilem  33458  qsdrngi  33459  rprmdvdsprod  33498  1arithidomlem1  33499  1arithidomlem2  33500  1arithidom  33501  1arithufdlem3  33510  dfufd2lem  33513  zringfrac  33518  evl1deg1  33538  evl1deg2  33539  evl1deg3  33540  ply1gsumz  33557  r1plmhm  33568  resssra  33576  ply1degltdimlem  33611  ply1degltdim  33612  qusdimsum  33617  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  lactlmhm  33623  fldgenfldext  33656  evls1fldgencl  33658  fldextrspunlsplem  33661  fldextrspundgdvdslem  33668  fldextrspundgdvds  33669  algextdeglem4  33703  algextdeglem6  33705  algextdeglem7  33706  submateq  33792  lmatcl  33799  mdetpmtr1  33806  madjusmdetlem1  33810  madjusmdetlem3  33812  qqhvval  33966  esumfzf  34052  esumpfinvallem  34057  esumpmono  34062  esummulc1  34064  esumcvg  34069  esumgect  34073  ofcval  34082  omssubadd  34284  sitgfval  34325  sitmcl  34335  sseqfv2  34378  cndprobval  34417  ballotlemfval  34474  ballotlemsv  34494  ballotlemsf1o  34498  ofcccat  34527  signsplypnf  34534  signsply0  34535  signstfval  34548  signshf  34572  reprpmtf1o  34610  reprdifc  34611  logdivsqrle  34634  hgt750lemg  34638  hgt750lema  34641  lpadval  34660  cvmliftlem8  35272  cvmliftphtlem  35297  fmla1  35367  gonarlem  35374  sategoelfvb  35399  mrsubval  35489  ellcsrspsn  35621  r1peuqusdeg1  35623  fwddifval  36143  knoppcnlem1  36474  knoppcnlem6  36479  unbdqndv2lem2  36491  poimirlem1  37608  poimirlem2  37609  poimirlem3  37610  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem16  37623  poimirlem19  37626  poimirlem22  37629  poimirlem23  37630  broucube  37641  dvtan  37657  itg2addnc  37661  ibladdnc  37664  itgaddnc  37667  itgmulc2nclem2  37674  itgmulc2nc  37675  itgabsnc  37676  ftc1cnnclem  37678  ftc1anclem3  37682  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anclem8  37687  dvasin  37691  dvacos  37692  dvreasin  37693  dvreacos  37694  areacirclem1  37695  areacirc  37700  fsumshftd  38938  hlrelat5N  39388  rhmzrhval  41952  aks6d1c1  42097  hashscontpow  42103  aks6d1c4  42105  aks6d1c2lem3  42107  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem0  42116  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c5  42120  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem1  42151  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6isolem3  42157  aks6d1c6lem5  42158  aks6d1c7lem2  42162  unitscyglem1  42176  readvrec2  42342  readvrec  42343  readvcot  42345  frlmfzolen  42484  frlmfzoccat  42486  frlmvscadiccat  42487  evlscl  42539  evlsval3  42540  evlsvval  42541  evlsvvval  42544  evlsbagval  42547  evlsexpval  42548  evlsaddval  42549  evlsmulval  42550  evlsevl  42552  evlcl  42553  evladdval  42556  evlmulval  42557  selvcl  42564  evlselv  42568  fsuppind  42571  mhpind  42575  mhphflem  42577  prjspner  42600  prjspnvs  42601  prjspnfv01  42605  prjspner01  42606  prjspner1  42607  0prjspnrel  42608  prjcrv0  42614  mzpclall  42708  mzpsubst  42729  eldioph2  42743  rabdiophlem2  42783  irrapxlem1  42803  mzpcong  42954  mendlmod  43171  naddcnff  43344  relexpmulnn  43691  iunrelexpuztr  43701  mnringvald  44195  mnringmulrvald  44209  radcnvrat  44296  hashnzfzclim  44304  lhe4.4ex1a  44311  expgrowthi  44315  expgrowth  44317  bccval  44320  binomcxplemrat  44332  binomcxplemfrat  44333  binomcxplemradcnv  44334  binomcxplemdvbinom  44335  binomcxplemdvsum  44337  binomcxplemnotnn0  44338  unirnmap  45195  unirnmapsn  45201  ssmapsn  45203  iocopn  45511  icoopn  45516  divcnvg  45618  sumnnodd  45621  climsubmpt  45651  dvsinax  45904  fperdvper  45910  dvdivf  45913  dvnprodlem1  45937  itgsincmulx  45965  stoweidlem59  46050  etransclem4  46229  etransclem13  46238  etransclem25  46250  etransclem48  46273  rrxtopnfi  46278  sge0tsms  46371  elhoi  46533  ovnval2  46536  ovnval2b  46543  ovncvrrp  46555  ovn0lem  46556  ovncl  46558  ovnome  46564  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvle  46591  ovnlecvr2  46601  ovncvr2  46602  ovnsubadd2lem  46636  ovnovollem1  46647  vonvolmbl  46652  iunhoiioolem  46666  vonioolem1  46671  vonioolem2  46672  vonicclem2  46675  smfresal  46779  smfres  46781  smfmullem4  46785  smfco  46793  adddmmbl  46824  muldmmbl  46826  sinnpoly  46885  fmtno  47523  isubgruhgr  47861  grtriprop  47933  grtriclwlk3  47937  gpgvtx  48027  gpgiedg  48028  intopval  48183  clintopval  48185  rngchomALTV  48249  funcringcsetcALTV2lem5  48275  ringchomALTV  48283  funcringcsetclem5ALTV  48298  srhmsubcALTVlem2  48305  srhmsubcALTV  48306  fldhmsubcALTV  48314  zlmodzxzscm  48338  zlmodzxzadd  48339  rmsupp0  48349  domnmsuppn0  48350  rmsuppss  48351  ply1mulgsumlem3  48370  ply1mulgsumlem4  48371  ply1mulgsum  48372  dmatALTval  48382  lincop  48390  lincval  48391  linc1  48407  lincresunit3lem1  48461  fdivmpt  48522  fdivmptfv  48527  refdivmptfv  48528  digval  48580  2arymptfv  48632  2arymaptfo  48636  itcovalpclem1  48652  itcovalt2lem1  48657  ackvalsuc1mpt  48660  ackval1  48663  ackval2  48664  ackval3  48665  ackval42  48678  line2xlem  48735  upfval2  49159  swapfval  49244  tposcurf1  49281  tposcurf2val  49283  fucofvalg  49300  fuco112x  49314  fuco23  49323  fucoid  49330  fucocolem4  49338  prcofvalg  49358  prcof1  49370  opf2fval  49387  lanval  49601  ranval  49602