Theorem ovexd 7395

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  (class class class)co 7360

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 2709  ax-nul 5252

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-sn 4582  df-pr 4584  df-uni 4865  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  caofidlcan  7662  caofass  7664  caofdi  7666  caofdir  7667  caonncan  7668  suppofssd  8147  mapsnend  8977  snmapen  8979  pw2eng  9015  mapen  9073  mapxpen  9075  mapunen  9078  mapdom2  9080  cantnfcl  9580  cantnfle  9584  cantnflt  9585  cantnflt2  9586  cantnfp1lem2  9592  cantnfp1lem3  9593  cantnflem1b  9599  cantnflem1d  9601  cantnflem1  9602  cnfcomlem  9612  cnfcom  9613  cnfcom2lem  9614  cnfcom3lem  9616  fzen  13461  seqf1o  13970  wrdexg  14451  wrdnval  14472  pfxval  14601  pfxswrd  14633  splval  14678  ofccat  14896  climshftlem  15501  climshft  15503  climshft2  15509  caucvgr  15603  fsumrev  15706  hashdvds  16706  setsabs  17110  ressress  17178  firest  17356  prdsvscafval  17404  qusval  17467  xpsbas  17497  xpsadd  17499  xpsmul  17500  xpssca  17501  xpsvsca  17502  xpsless  17503  xpsle  17504  homfval  17619  comfval  17627  cicfval  17725  rescabs  17761  rescabs2  17762  resscat  17780  funcres2c  17831  ressffth  17868  fucbas  17891  fuccoval  17894  setchom  18008  catchom  18031  catcco  18033  estrchom  18054  funcestrcsetclem5  18071  funcsetcestrclem5  18086  evlf2val  18146  curf11  18153  curf12  18154  curf2val  18157  uncfval  18161  diagval  18167  hof2  18184  yonval  18188  resspos  18356  gsumval2a  18614  gsumval2  18615  mndpsuppss  18694  gsumwspan  18775  efmnd  18799  ghmqusnsglem1  19213  ghmqusnsglem2  19214  ghmqusnsg  19215  ghmquskerlem1  19216  ghmquskerco  19217  ghmquskerlem2  19218  ghmquskerlem3  19219  ghmqusker  19220  orbstafun  19244  orbstaval  19245  symgval  19304  psgnvalii  19442  lsmhash  19638  frgpupval  19707  qusabl  19798  gsumval3  19840  gsumreidx  19850  gsumzaddlem  19854  gsummptshft  19869  telgsumfzslem  19921  telgsumfz  19923  telgsumfz0  19925  dpjval  19991  prdsrngd  20115  srgbinomlem3  20167  srgbinomlem4  20168  mulgass3  20293  rngcval  20555  rnghmsscmap2  20566  rnghmsscmap  20567  funcrngcsetc  20577  ringcval  20584  rhmsscmap2  20595  rhmsscmap  20596  funcringcsetc  20611  srhmsubclem3  20616  srhmsubc  20617  fldhmsubc  20722  lcomfsupp  20857  rmodislmodlem  20884  rmodislmod  20885  sraval  21131  srasca  21136  crngridl  21239  quscrng  21242  rhmqusnsg  21244  pzriprnglem11  21450  znval  21494  znzrhfo  21506  znunithash  21523  cygznlem2  21527  frobrhm  21534  pjfval  21665  pjpm  21667  frlmgsum  21731  frlmipval  21738  frlmphllem  21739  frlmphl  21740  frlmsslsp  21755  frlmup1  21757  gsumbagdiaglem  21890  psrass1lem  21892  rhmpsrlem1  21900  psrass1  21923  psrdi  21924  psrdir  21925  psrass23l  21926  psrascl  21938  mplval  21948  mplsubglem  21958  mplsubrglem  21963  mplmonmul  21995  mplcoe1  21996  opsrval  22005  psrbagev1  22036  psrbagev2  22037  evlslem6  22040  evlslem1  22041  evlsval  22045  evlsval3  22048  evlsvval  22049  evlsvvval  22052  evlcl  22061  evladdval  22062  evlmulval  22063  mpfconst  22068  mpff  22071  mpfaddcl  22072  mpfmulcl  22073  mpfind  22074  mhpmulcl  22096  mhpaddcl  22098  psdcoef  22107  psdmplcl  22109  psdadd  22110  ply1lss  22141  gsumply1subr  22178  coe1add  22210  coe1tm  22219  coe1tmmul  22223  cply1mul  22244  ply1coe  22246  evl1expd  22293  pf1mpf  22300  pf1ind  22303  mhmcompl  22328  mhmcoaddmpl  22329  rhmmpl  22331  rhmply1vsca  22336  mamufv  22342  mamuass  22350  mamuvs1  22353  mamuvs2  22354  matgsum  22385  dmatmul  22445  scmatval  22452  scmatrhmval  22475  mvmulfv  22492  mavmulfv  22494  mavmulass  22497  marrepeval  22511  marepveval  22516  submaeval  22530  mdetrsca  22551  mdetunilem9  22568  mdetuni0  22569  gsummatr01lem3  22605  gsummatr01lem4  22606  gsummatr01  22607  smadiadetlem3  22616  cramerlem1  22635  mat2pmatmul  22679  m2cpminvid  22701  decpmatfsupp  22717  decpmatmullem  22719  decpmatmul  22720  decpmatmulsumfsupp  22721  pmatcollpw1lem1  22722  pmatcollpw3fi1lem1  22734  pmatcollpwscmatlem2  22738  pm2mpfval  22744  pm2mpf  22746  mply1topmatcllem  22751  mp2pm2mplem3  22756  mp2pm2mplem4  22757  pm2mpmhmlem1  22766  pm2mpmhmlem2  22767  pm2mp  22773  chfacfscmulfsupp  22807  chfacfscmulgsum  22808  chfacfpmmulfsupp  22811  chfacfpmmulgsum  22812  cpmidpmatlem3  22820  cpmadugsumlemB  22822  cpmadugsumlemC  22823  cpmadugsumlemF  22824  cayhamlem4  22836  xpstopnlem2  23759  fcfval  23981  tsmsxplem1  24101  tsmsxplem2  24102  tusval  24213  xpsdsfn  24325  xpsxmet  24328  xpsdsval  24329  xpsmet  24330  tmsval  24429  met1stc  24469  metuval  24497  cnmpopc  24882  pi1val  24997  pi1addf  25007  pi1addval  25008  pi1grplem  25009  rrxnm  25351  rrxcph  25352  rrxmval  25365  mbfmulc2  25624  mbfmul  25687  itg2mulclem  25707  ibladd  25782  itgadd  25786  itgabs  25796  bddmulibl  25800  dvmulf  25906  dvcmulf  25908  dvmptmul  25925  cmvth  25955  dvlip  25958  ftc1lem4  26006  mdegmullem  26043  coe1mul3  26064  r1pval  26123  plyco  26206  dgrcolem1  26239  elqaalem3  26289  taylpfval  26332  taylthlem2  26342  taylthlem2OLD  26343  pserdvlem2  26398  advlogexp  26624  logtayl  26629  logccv  26632  dvcxp1  26709  dvcncxp1  26712  logbmpt  26758  logbfval  26760  relogbf  26761  dvatan  26905  cxp2lim  26947  cxploglim2  26949  lgamgulmlem2  27000  lgamgulm2  27006  lgamcvglem  27010  lgamf  27012  basellem7  27057  basellem8  27058  basellem9  27059  fsumdvdscom  27155  logexprlim  27196  dchrfi  27226  gausslemma2dlem2  27338  gausslemma2dlem3  27339  2lgslem1b  27363  chtppilimlem2  27445  chebbnd2  27448  chto1lb  27449  chpchtlim  27450  chpo1ub  27451  vmadivsum  27453  dchrisum0lem3  27490  mudivsum  27501  logdivsum  27504  log2sumbnd  27515  selberglem1  27516  selberg2lem  27521  selberg2  27522  selbergr  27539  negsval  28025  wlkp1  29757  cyclnumvtx  29877  wwlksnextsurj  29977  wwlksnextbij  29979  clwlkclwwlklem2a1  30071  clwlkclwwlkf1  30089  eupth2eucrct  30296  frgrncvvdeq  30388  numclwlk2lem2fv  30457  numclwwlk2lem3  30459  ofoprabco  32745  fsuppcurry1  32805  fsuppcurry2  32806  offinsupp1  32807  ressprs  33050  mntoval  33066  mgcoval  33070  mndlactf1  33110  mndlactfo  33111  mndractf1  33112  mndractfo  33113  mndlactf1o  33114  mndractf1o  33115  lmodvslmhm  33135  gsummulsubdishift2  33154  gsumwrd2dccat  33162  cycpmco2f1  33208  cycpmco2rn  33209  cycpmco2lem2  33211  cycpmco2lem3  33212  cycpmco2lem4  33213  cycpmco2lem5  33214  cycpmco2lem6  33215  cycpmco2  33217  conjga  33254  cntrval2  33255  fxpsubm  33256  fxpsubg  33257  fxpsubrg  33258  fxpsdrg  33259  archirngz  33273  archiabllem2a  33278  elrgspnlem1  33326  elrgspnlem2  33327  elrgspnsubrunlem2  33332  rlocval  33343  fracval  33388  quslmod  33441  quslmhm  33442  quslvec  33443  qustriv  33447  qustrivr  33448  unitprodclb  33472  nsgmgc  33495  nsgqusf1olem1  33496  nsgqusf1olem2  33497  nsgqusf1olem3  33498  lmhmqusker  33500  rhmquskerlem  33508  elrspunidl  33511  qsidomlem1  33535  qsidomlem2  33536  opprqusbas  33571  opprqusplusg  33572  opprqusmulr  33574  opprqus1r  33575  qsdrngilem  33577  qsdrngi  33578  rprmdvdsprod  33617  1arithidomlem1  33618  1arithidomlem2  33619  1arithidom  33620  1arithufdlem3  33629  dfufd2lem  33632  zringfrac  33637  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  ply1gsumz  33682  r1plmhm  33693  mplvrpmrhm  33714  splyval  33719  vietadeg1  33736  resssra  33745  ply1degltdimlem  33781  ply1degltdim  33782  qusdimsum  33787  fedgmullem1  33788  fedgmullem2  33789  fedgmul  33790  lactlmhm  33793  fldgenfldext  33827  evls1fldgencl  33829  fldextrspunlsplem  33832  fldextrspundgdvdslem  33839  fldextrspundgdvds  33840  extdgfialglem1  33851  extdgfialglem2  33852  extdgfialg  33853  algextdeglem4  33879  algextdeglem6  33881  algextdeglem7  33882  submateq  33968  lmatcl  33975  mdetpmtr1  33982  madjusmdetlem1  33986  madjusmdetlem3  33988  qqhvval  34142  esumfzf  34228  esumpfinvallem  34233  esumpmono  34238  esummulc1  34240  esumcvg  34245  esumgect  34249  ofcval  34258  omssubadd  34459  sitgfval  34500  sitmcl  34510  sseqfv2  34553  cndprobval  34592  ballotlemfval  34649  ballotlemsv  34669  ballotlemsf1o  34673  ofcccat  34702  signsplypnf  34709  signsply0  34710  signstfval  34723  signshf  34747  reprpmtf1o  34785  reprdifc  34786  logdivsqrle  34809  hgt750lemg  34813  hgt750lema  34816  lpadval  34835  cvmliftlem8  35488  cvmliftphtlem  35513  fmla1  35583  gonarlem  35590  sategoelfvb  35615  mrsubval  35705  ellcsrspsn  35837  r1peuqusdeg1  35839  fwddifval  36358  knoppcnlem1  36695  knoppcnlem6  36700  unbdqndv2lem2  36712  poimirlem1  37824  poimirlem2  37825  poimirlem3  37826  poimirlem5  37828  poimirlem6  37829  poimirlem7  37830  poimirlem10  37833  poimirlem11  37834  poimirlem12  37835  poimirlem16  37839  poimirlem19  37842  poimirlem22  37845  poimirlem23  37846  broucube  37857  dvtan  37873  itg2addnc  37877  ibladdnc  37880  itgaddnc  37883  itgmulc2nclem2  37890  itgmulc2nc  37891  itgabsnc  37892  ftc1cnnclem  37894  ftc1anclem3  37898  ftc1anclem6  37901  ftc1anclem7  37902  ftc1anclem8  37903  dvasin  37907  dvacos  37908  dvreasin  37909  dvreacos  37910  areacirclem1  37911  areacirc  37916  fsumshftd  39280  hlrelat5N  39729  rhmzrhval  42293  aks6d1c1  42438  hashscontpow  42444  aks6d1c4  42446  aks6d1c2lem3  42448  aks6d1c2lem4  42449  aks6d1c2  42452  aks6d1c5lem0  42457  aks6d1c5lem3  42459  aks6d1c5lem2  42460  aks6d1c5  42461  sticksstones3  42470  sticksstones8  42475  sticksstones10  42477  sticksstones12a  42479  sticksstones12  42480  aks6d1c6lem1  42492  aks6d1c6lem2  42493  aks6d1c6lem3  42494  aks6d1c6lem4  42495  aks6d1c6isolem1  42496  aks6d1c6isolem2  42497  aks6d1c6isolem3  42498  aks6d1c6lem5  42499  aks6d1c7lem2  42503  unitscyglem1  42517  readvrec2  42683  readvrec  42684  readvcot  42686  frlmfzolen  42825  frlmfzoccat  42827  frlmvscadiccat  42828  evlscl  42876  evlsbagval  42879  evlsexpval  42880  evlsaddval  42881  evlsmulval  42882  evlsevl  42884  selvcl  42893  evlselv  42897  fsuppind  42900  mhpind  42904  mhphflem  42906  prjspner  42929  prjspnvs  42930  prjspnfv01  42934  prjspner01  42935  prjspner1  42936  0prjspnrel  42937  prjcrv0  42943  mzpclall  43036  mzpsubst  43057  eldioph2  43071  rabdiophlem2  43111  irrapxlem1  43131  mzpcong  43281  mendlmod  43498  naddcnff  43671  relexpmulnn  44017  iunrelexpuztr  44027  mnringvald  44521  mnringmulrvald  44535  radcnvrat  44622  hashnzfzclim  44630  lhe4.4ex1a  44637  expgrowthi  44641  expgrowth  44643  bccval  44646  binomcxplemrat  44658  binomcxplemfrat  44659  binomcxplemradcnv  44660  binomcxplemdvbinom  44661  binomcxplemdvsum  44663  binomcxplemnotnn0  44664  unirnmap  45519  unirnmapsn  45525  ssmapsn  45527  iocopn  45833  icoopn  45838  divcnvg  45940  sumnnodd  45943  climsubmpt  45971  dvsinax  46224  fperdvper  46230  dvdivf  46233  dvnprodlem1  46257  itgsincmulx  46285  stoweidlem59  46370  etransclem4  46549  etransclem13  46558  etransclem25  46570  etransclem48  46593  rrxtopnfi  46598  sge0tsms  46691  elhoi  46853  ovnval2  46856  ovnval2b  46863  ovncvrrp  46875  ovn0lem  46876  ovncl  46878  ovnome  46884  hoidmvlelem2  46907  hoidmvlelem3  46908  hoidmvle  46911  ovnlecvr2  46921  ovncvr2  46922  ovnsubadd2lem  46956  ovnovollem1  46967  vonvolmbl  46972  iunhoiioolem  46986  vonioolem1  46991  vonioolem2  46992  vonicclem2  46995  smfresal  47099  smfres  47101  smfmullem4  47105  smfco  47113  adddmmbl  47144  muldmmbl  47146  chnsuslle  47192  nthrucw  47197  sinnpoly  47204  fmtno  47842  isubgruhgr  48181  grtriprop  48254  grtriclwlk3  48258  gpgvtx  48356  gpgiedg  48357  intopval  48515  clintopval  48517  rngchomALTV  48581  funcringcsetcALTV2lem5  48607  ringchomALTV  48615  funcringcsetclem5ALTV  48630  srhmsubcALTVlem2  48637  srhmsubcALTV  48638  fldhmsubcALTV  48646  zlmodzxzscm  48670  zlmodzxzadd  48671  rmsupp0  48681  domnmsuppn0  48682  rmsuppss  48683  ply1mulgsumlem3  48701  ply1mulgsumlem4  48702  ply1mulgsum  48703  dmatALTval  48713  lincop  48721  lincval  48722  linc1  48738  lincresunit3lem1  48792  fdivmpt  48853  fdivmptfv  48858  refdivmptfv  48859  digval  48911  2arymptfv  48963  2arymaptfo  48967  itcovalpclem1  48983  itcovalt2lem1  48988  ackvalsuc1mpt  48991  ackval1  48994  ackval2  48995  ackval3  48996  ackval42  49009  line2xlem  49066  upfval2  49489  swapfval  49574  tposcurf1  49611  tposcurf2val  49613  fucofvalg  49630  fuco112x  49644  fuco23  49653  fucoid  49660  fucocolem4  49668  prcofvalg  49688  prcof1  49700  opf2fval  49717  lanval  49931  ranval  49932