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 2121  Vcvv 3433  (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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5231

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-sn 4559  df-pr 4561  df-uni 4842  df-iota 6445  df-fv 6497  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  9583  cantnfle  9587  cantnflt  9588  cantnflt2  9589  cantnfp1lem2  9595  cantnfp1lem3  9596  cantnflem1b  9602  cantnflem1d  9604  cantnflem1  9605  cnfcomlem  9615  cnfcom  9616  cnfcom2lem  9617  cnfcom3lem  9619  fzen  13490  seqf1o  14000  wrdexg  14481  wrdnval  14502  pfxval  14631  pfxswrd  14663  splval  14708  ofccat  14926  climshftlem  15531  climshft  15533  climshft2  15539  caucvgr  15633  fsumrev  15736  hashdvds  16740  setsabs  17144  ressress  17212  firest  17390  prdsvscafval  17438  qusval  17501  xpsbas  17531  xpsadd  17533  xpsmul  17534  xpssca  17535  xpsvsca  17536  xpsless  17537  xpsle  17538  homfval  17653  comfval  17661  cicfval  17759  rescabs  17795  rescabs2  17796  resscat  17814  funcres2c  17865  ressffth  17902  fucbas  17925  fuccoval  17928  setchom  18042  catchom  18065  catcco  18067  estrchom  18088  funcestrcsetclem5  18105  funcsetcestrclem5  18120  evlf2val  18180  curf11  18187  curf12  18188  curf2val  18191  uncfval  18195  diagval  18201  hof2  18218  yonval  18222  resspos  18390  gsumval2a  18648  gsumval2  18649  mndpsuppss  18728  gsumwspan  18809  efmnd  18833  ghmqusnsglem1  19250  ghmqusnsglem2  19251  ghmqusnsg  19252  ghmquskerlem1  19253  ghmquskerco  19254  ghmquskerlem2  19255  ghmquskerlem3  19256  ghmqusker  19257  orbstafun  19281  orbstaval  19282  symgval  19341  psgnvalii  19479  lsmhash  19675  frgpupval  19744  qusabl  19835  gsumval3  19877  gsumreidx  19887  gsumzaddlem  19891  gsummptshft  19906  telgsumfzslem  19958  telgsumfz  19960  telgsumfz0  19962  dpjval  20028  prdsrngd  20152  srgbinomlem3  20204  srgbinomlem4  20205  mulgass3  20328  rngcval  20594  rnghmsscmap2  20605  rnghmsscmap  20606  funcrngcsetc  20616  ringcval  20623  rhmsscmap2  20634  rhmsscmap  20635  funcringcsetc  20650  srhmsubclem3  20655  srhmsubc  20656  fldhmsubc  20761  lcomfsupp  20896  rmodislmodlem  20923  rmodislmod  20924  sraval  21169  srasca  21174  crngridl  21277  quscrng  21280  rhmqusnsg  21282  pzriprnglem11  21470  znval  21514  znzrhfo  21526  znunithash  21543  cygznlem2  21547  frobrhm  21554  pjfval  21685  pjpm  21687  frlmgsum  21751  frlmipval  21758  frlmphllem  21759  frlmphl  21760  frlmsslsp  21775  frlmup1  21777  gsumbagdiaglem  21910  psrass1lem  21912  rhmpsrlem1  21919  psrass1  21942  psrdi  21943  psrdir  21944  psrass23l  21945  psrascl  21957  mplval  21967  mplsubglem  21977  mplsubrglem  21982  mplmonmul  22016  mplcoe1  22017  opsrval  22026  psrbagev1  22057  psrbagev2  22058  evlslem6  22061  evlslem1  22062  evlsval  22066  evlsval3  22069  evlsvval  22070  evlsvvval  22073  evlcl  22082  evladdval  22083  evlmulval  22084  mpfconst  22089  mpff  22092  mpfaddcl  22093  mpfmulcl  22094  mpfind  22095  mhmcompl  22101  mhmcoaddmpl  22103  evlscl  22105  evlsexpval  22108  evlsaddval  22109  evlsmulval  22110  evlsevl  22112  selvcl  22120  mhpmulcl  22141  mhpaddcl  22143  psdcoef  22152  psdmplcl  22154  psdadd  22155  ply1lss  22185  gsumply1subr  22222  coe1add  22254  coe1tm  22263  coe1tmmul  22267  cply1mul  22286  ply1coe  22288  evl1expd  22335  pf1mpf  22342  pf1ind  22345  rhmmpl  22370  rhmply1vsca  22375  mamufv  22381  mamuass  22389  mamuvs1  22392  mamuvs2  22393  matgsum  22424  dmatmul  22484  scmatval  22491  scmatrhmval  22514  mvmulfv  22531  mavmulfv  22533  mavmulass  22536  marrepeval  22550  marepveval  22555  submaeval  22569  mdetrsca  22590  mdetunilem9  22607  mdetuni0  22608  gsummatr01lem3  22644  gsummatr01lem4  22645  gsummatr01  22646  smadiadetlem3  22655  cramerlem1  22674  mat2pmatmul  22718  m2cpminvid  22740  decpmatfsupp  22756  decpmatmullem  22758  decpmatmul  22759  decpmatmulsumfsupp  22760  pmatcollpw1lem1  22761  pmatcollpw3fi1lem1  22773  pmatcollpwscmatlem2  22777  pm2mpfval  22783  pm2mpf  22785  mply1topmatcllem  22790  mp2pm2mplem3  22795  mp2pm2mplem4  22796  pm2mpmhmlem1  22805  pm2mpmhmlem2  22806  pm2mp  22812  chfacfscmulfsupp  22846  chfacfscmulgsum  22847  chfacfpmmulfsupp  22850  chfacfpmmulgsum  22851  cpmidpmatlem3  22859  cpmadugsumlemB  22861  cpmadugsumlemC  22862  cpmadugsumlemF  22863  cayhamlem4  22875  xpstopnlem2  23798  fcfval  24020  tsmsxplem1  24140  tsmsxplem2  24141  tusval  24252  xpsdsfn  24364  xpsxmet  24367  xpsdsval  24368  xpsmet  24369  tmsval  24468  met1stc  24508  metuval  24536  cnmpopc  24917  pi1val  25026  pi1addf  25036  pi1addval  25037  pi1grplem  25038  rrxnm  25380  rrxcph  25381  rrxmval  25394  mbfmulc2  25652  mbfmul  25715  itg2mulclem  25735  ibladd  25810  itgadd  25814  itgabs  25824  bddmulibl  25828  dvmulf  25932  dvcmulf  25934  dvmptmul  25950  cmvth  25980  dvlip  25982  ftc1lem4  26028  mdegmullem  26065  coe1mul3  26086  r1pval  26145  plyco  26228  dgrcolem1  26260  elqaalem3  26309  taylpfval  26352  taylthlem2  26361  pserdvlem2  26415  advlogexp  26641  logtayl  26646  logccv  26649  dvcxp1  26726  dvcncxp1  26729  logbmpt  26774  logbfval  26776  relogbf  26777  dvatan  26921  cxp2lim  26962  cxploglim2  26964  lgamgulmlem2  27015  lgamgulm2  27021  lgamcvglem  27025  lgamf  27027  basellem7  27072  basellem8  27073  basellem9  27074  fsumdvdscom  27170  logexprlim  27210  dchrfi  27240  gausslemma2dlem2  27352  gausslemma2dlem3  27353  2lgslem1b  27377  chtppilimlem2  27459  chebbnd2  27462  chto1lb  27463  chpchtlim  27464  chpo1ub  27465  vmadivsum  27467  dchrisum0lem3  27504  mudivsum  27515  logdivsum  27518  log2sumbnd  27529  selberglem1  27530  selberg2lem  27535  selberg2  27536  selbergr  27553  negsval  28039  wlkp1  29770  cyclnumvtx  29890  wwlksnextsurj  29990  wwlksnextbij  29992  clwlkclwwlklem2a1  30084  clwlkclwwlkf1  30102  eupth2eucrct  30309  frgrncvvdeq  30401  numclwlk2lem2fv  30470  numclwwlk2lem3  30472  ofoprabco  32760  fsuppcurry1  32820  fsuppcurry2  32821  offinsupp1  32822  ressprs  33049  mntoval  33065  mgcoval  33069  mndlactf1  33109  mndlactfo  33110  mndractf1  33111  mndractfo  33112  mndlactf1o  33113  mndractf1o  33114  lmodvslmhm  33135  gsummulsubdishift2  33154  gsumwrd2dccat  33163  cycpmco2f1  33209  cycpmco2rn  33210  cycpmco2lem2  33212  cycpmco2lem3  33213  cycpmco2lem4  33214  cycpmco2lem5  33215  cycpmco2lem6  33216  cycpmco2  33218  conjga  33255  cntrval2  33256  fxpsubm  33257  fxpsubg  33258  fxpsubrg  33259  fxpsdrg  33260  archirngz  33274  archiabllem2a  33279  elrgspnlem1  33327  elrgspnlem2  33328  elrgspnsubrunlem2  33333  rlocval  33344  fracval  33392  quslmod  33445  quslmhm  33446  quslvec  33447  qustriv  33451  qustrivr  33452  unitprodclb  33476  nsgmgc  33499  nsgqusf1olem1  33500  nsgqusf1olem2  33501  nsgqusf1olem3  33502  lmhmqusker  33504  rhmquskerlem  33512  elrspunidl  33515  qsidomlem1  33539  qsidomlem2  33540  opprqusbas  33575  opprqusplusg  33576  opprqusmulr  33578  opprqus1r  33579  qsdrngilem  33581  qsdrngi  33582  rprmdvdsprod  33629  1arithidomlem1  33630  1arithidomlem2  33631  1arithidom  33632  1arithufdlem3  33641  dfufd2lem  33644  zringfrac  33649  evl1deg1  33671  evl1deg2  33672  evl1deg3  33673  ply1gsumz  33694  r1plmhm  33705  0mplrim  33710  selvply1rhmlema  33714  selvply1rhmlemb  33715  selvply1rhmlem1  33716  selvply1rhmlem3  33718  selvply1rhmlem4  33719  selvply1rhmlem5  33720  mplvrpmrhm  33743  psrgsum  33744  psrmonmul  33746  psrmonprod  33748  mplgsum  33749  splyval  33755  esplyfval1  33769  esplyfvaln  33770  vietadeg1  33774  resssra  33783  ply1degltdimlem  33818  ply1degltdim  33819  qusdimsum  33824  fedgmullem1  33825  fedgmullem2  33826  fedgmul  33827  lactlmhm  33830  fldgenfldext  33864  evls1fldgencl  33866  fldextrspunlsplem  33869  fldextrspundgdvdslem  33876  fldextrspundgdvds  33877  extdgfialglem1  33888  extdgfialglem2  33889  extdgfialg  33890  algextdeglem4  33916  algextdeglem6  33918  algextdeglem7  33919  submateq  34005  lmatcl  34012  mdetpmtr1  34019  madjusmdetlem1  34023  madjusmdetlem3  34025  qqhvval  34179  esumfzf  34265  esumpfinvallem  34270  esumpmono  34275  esummulc1  34277  esumcvg  34282  esumgect  34286  ofcval  34295  omssubadd  34496  sitgfval  34537  sitmcl  34547  sseqfv2  34590  cndprobval  34629  ballotlemfval  34686  ballotlemsv  34706  ballotlemsf1o  34710  ofcccat  34739  signsplypnf  34746  signsply0  34747  signstfval  34760  signshf  34784  reprpmtf1o  34822  reprdifc  34823  logdivsqrle  34846  hgt750lemg  34850  hgt750lema  34853  lpadval  34875  cvmliftlem8  35535  cvmliftphtlem  35560  fmla1  35630  gonarlem  35637  sategoelfvb  35662  mrsubval  35752  ellcsrspsn  35884  r1peuqusdeg1  35886  fwddifval  36405  knoppcnlem1  36814  knoppcnlem6  36819  unbdqndv2lem2  36831  poimirlem1  38003  poimirlem2  38004  poimirlem3  38005  poimirlem5  38007  poimirlem6  38008  poimirlem7  38009  poimirlem10  38012  poimirlem11  38013  poimirlem12  38014  poimirlem16  38018  poimirlem19  38021  poimirlem22  38024  poimirlem23  38025  broucube  38036  dvtan  38052  itg2addnc  38056  ibladdnc  38059  itgaddnc  38062  itgmulc2nclem2  38069  itgmulc2nc  38070  itgabsnc  38071  ftc1cnnclem  38073  ftc1anclem3  38077  ftc1anclem6  38080  ftc1anclem7  38081  ftc1anclem8  38082  dvasin  38086  dvacos  38087  dvreasin  38088  dvreacos  38089  areacirclem1  38090  areacirc  38095  fsumshftd  39459  hlrelat5N  39908  rhmzrhval  42472  aks6d1c1  42616  hashscontpow  42622  aks6d1c4  42624  aks6d1c2lem3  42626  aks6d1c2lem4  42627  aks6d1c2  42630  aks6d1c5lem0  42635  aks6d1c5lem3  42637  aks6d1c5lem2  42638  aks6d1c5  42639  sticksstones3  42648  sticksstones8  42653  sticksstones10  42655  sticksstones12a  42657  sticksstones12  42658  aks6d1c6lem1  42670  aks6d1c6lem2  42671  aks6d1c6lem3  42672  aks6d1c6lem4  42673  aks6d1c6isolem1  42674  aks6d1c6isolem2  42675  aks6d1c6isolem3  42676  aks6d1c6lem5  42677  aks6d1c7lem2  42681  unitscyglem1  42695  readvrec2  42853  readvrec  42854  readvcot  42856  frlmfzolen  43008  frlmfzoccat  43010  frlmvscadiccat  43011  evlsbagval  43051  evlselv  43054  fsuppind  43055  mhpind  43059  mhphflem  43061  prjspner  43084  prjspnvs  43085  prjspnfv01  43089  prjspner01  43090  prjspner1  43091  0prjspnrel  43092  prjcrv0  43098  mzpclall  43191  mzpsubst  43212  eldioph2  43226  rabdiophlem2  43262  irrapxlem1  43282  mzpcong  43432  mendlmod  43649  naddcnff  43822  relexpmulnn  44168  iunrelexpuztr  44178  mnringvald  44672  mnringmulrvald  44686  radcnvrat  44773  hashnzfzclim  44781  lhe4.4ex1a  44788  expgrowthi  44792  expgrowth  44794  bccval  44797  binomcxplemrat  44809  binomcxplemfrat  44810  binomcxplemradcnv  44811  binomcxplemdvbinom  44812  binomcxplemdvsum  44814  binomcxplemnotnn0  44815  unirnmap  45667  unirnmapsn  45673  ssmapsn  45675  iocopn  45979  icoopn  45984  divcnvg  46086  sumnnodd  46089  climsubmpt  46117  dvsinax  46370  fperdvper  46376  dvdivf  46379  dvnprodlem1  46403  itgsincmulx  46431  stoweidlem59  46516  etransclem4  46695  etransclem13  46704  etransclem25  46716  etransclem48  46739  rrxtopnfi  46744  sge0tsms  46837  elhoi  46999  ovnval2  47002  ovnval2b  47009  ovncvrrp  47021  ovn0lem  47022  ovncl  47024  ovnome  47030  hoidmvlelem2  47053  hoidmvlelem3  47054  hoidmvle  47057  ovnlecvr2  47067  ovncvr2  47068  ovnsubadd2lem  47102  ovnovollem1  47113  vonvolmbl  47118  iunhoiioolem  47132  vonioolem1  47137  vonioolem2  47138  vonicclem2  47141  smfresal  47245  smfres  47247  smfmullem4  47251  smfco  47259  adddmmbl  47290  muldmmbl  47292  chnsuslle  47340  nthrucw  47345  sinnpoly  47368  fmtno  48021  isubgruhgr  48373  grtriprop  48446  grtriclwlk3  48450  gpgvtx  48548  gpgiedg  48549  intopval  48707  clintopval  48709  rngchomALTV  48773  funcringcsetcALTV2lem5  48799  ringchomALTV  48807  funcringcsetclem5ALTV  48822  srhmsubcALTVlem2  48829  srhmsubcALTV  48830  fldhmsubcALTV  48838  zlmodzxzscm  48862  zlmodzxzadd  48863  rmsupp0  48873  domnmsuppn0  48874  rmsuppss  48875  ply1mulgsumlem3  48893  ply1mulgsumlem4  48894  ply1mulgsum  48895  dmatALTval  48905  lincop  48913  lincval  48914  linc1  48930  lincresunit3lem1  48984  fdivmpt  49045  fdivmptfv  49050  refdivmptfv  49051  digval  49103  2arymptfv  49155  2arymaptfo  49159  itcovalpclem1  49175  itcovalt2lem1  49180  ackvalsuc1mpt  49183  ackval1  49186  ackval2  49187  ackval3  49188  ackval42  49201  line2xlem  49258  upfval2  49681  swapfval  49766  tposcurf1  49803  tposcurf2val  49805  fucofvalg  49822  fuco112x  49836  fuco23  49845  fucoid  49852  fucocolem4  49860  prcofvalg  49880  prcof1  49892  opf2fval  49909  lanval  50123  ranval  50124