Theorem ovexd 7438

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459  (class class class)co 7403

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-sn 4602  df-pr 4604  df-uni 4884  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  caofidlcan  7707  caofass  7709  caofdi  7711  caofdir  7712  caonncan  7713  suppofssd  8200  mapsnend  9048  snmapen  9050  pw2eng  9090  mapen  9153  mapxpen  9155  mapunen  9158  mapdom2  9160  cantnfcl  9679  cantnfle  9683  cantnflt  9684  cantnflt2  9685  cantnfp1lem2  9691  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1d  9700  cantnflem1  9701  cnfcomlem  9711  cnfcom  9712  cnfcom2lem  9713  cnfcom3lem  9715  fzen  13556  seqf1o  14059  wrdexg  14540  wrdnval  14561  pfxval  14689  pfxswrd  14722  splval  14767  cshwsexaOLD  14841  ofccat  14986  climshftlem  15588  climshft  15590  climshft2  15596  caucvgr  15690  fsumrev  15793  hashdvds  16792  setsabs  17196  ressress  17266  firest  17444  prdsvscafval  17492  qusval  17554  xpsbas  17584  xpsadd  17586  xpsmul  17587  xpssca  17588  xpsvsca  17589  xpsless  17590  xpsle  17591  homfval  17702  comfval  17710  cicfval  17808  rescabs  17844  rescabs2  17845  resscat  17863  funcres2c  17914  ressffth  17951  fucbas  17974  fuccoval  17977  setchom  18091  catchom  18114  catcco  18116  estrchom  18137  funcestrcsetclem5  18154  funcsetcestrclem5  18169  evlf2val  18229  curf11  18236  curf12  18237  curf2val  18240  uncfval  18244  diagval  18250  hof2  18267  yonval  18271  gsumval2a  18661  gsumval2  18662  mndpsuppss  18741  gsumwspan  18822  efmnd  18846  ghmqusnsglem1  19261  ghmqusnsglem2  19262  ghmqusnsg  19263  ghmquskerlem1  19264  ghmquskerco  19265  ghmquskerlem2  19266  ghmquskerlem3  19267  ghmqusker  19268  orbstafun  19292  orbstaval  19293  symgval  19350  psgnvalii  19488  lsmhash  19684  frgpupval  19753  qusabl  19844  gsumval3  19886  gsumreidx  19896  gsumzaddlem  19900  gsummptshft  19915  telgsumfzslem  19967  telgsumfz  19969  telgsumfz0  19971  dpjval  20037  prdsrngd  20134  srgbinomlem3  20186  srgbinomlem4  20187  mulgass3  20311  rngcval  20576  rnghmsscmap2  20587  rnghmsscmap  20588  funcrngcsetc  20598  ringcval  20605  rhmsscmap2  20616  rhmsscmap  20617  funcringcsetc  20632  srhmsubclem3  20637  srhmsubc  20638  fldhmsubc  20743  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  21664  pjpm  21666  frlmgsum  21730  frlmipval  21737  frlmphllem  21738  frlmphl  21739  frlmsslsp  21754  frlmup1  21756  gsumbagdiaglem  21888  psrass1lem  21890  rhmpsrlem1  21898  psrass1  21922  psrdi  21923  psrdir  21924  psrass23l  21925  psrascl  21937  mplval  21947  mplsubglem  21957  mplsubrglem  21962  mplmonmul  21992  mplcoe1  21993  opsrval  22002  psrbagev1  22033  psrbagev2  22034  evlslem6  22037  evlslem1  22038  evlsval  22042  mpfconst  22057  mpff  22060  mpfaddcl  22061  mpfmulcl  22062  mpfind  22063  mhpmulcl  22085  mhpaddcl  22087  psdcoef  22096  psdmplcl  22098  psdadd  22099  ply1lss  22130  gsumply1subr  22167  coe1add  22199  coe1tm  22208  coe1tmmul  22212  cply1mul  22232  ply1coe  22234  evl1expd  22281  pf1mpf  22288  pf1ind  22291  mhmcompl  22316  mhmcoaddmpl  22317  rhmmpl  22319  rhmply1vsca  22324  mamufv  22330  mamuass  22338  mamuvs1  22341  mamuvs2  22342  matgsum  22373  dmatmul  22433  scmatval  22440  scmatrhmval  22463  mvmulfv  22480  mavmulfv  22482  mavmulass  22485  marrepeval  22499  marepveval  22504  submaeval  22518  mdetrsca  22539  mdetunilem9  22556  mdetuni0  22557  gsummatr01lem3  22593  gsummatr01lem4  22594  gsummatr01  22595  smadiadetlem3  22604  cramerlem1  22623  mat2pmatmul  22667  m2cpminvid  22689  decpmatfsupp  22705  decpmatmullem  22707  decpmatmul  22708  decpmatmulsumfsupp  22709  pmatcollpw1lem1  22710  pmatcollpw3fi1lem1  22722  pmatcollpwscmatlem2  22726  pm2mpfval  22732  pm2mpf  22734  mply1topmatcllem  22739  mp2pm2mplem3  22744  mp2pm2mplem4  22745  pm2mpmhmlem1  22754  pm2mpmhmlem2  22755  pm2mp  22761  chfacfscmulfsupp  22795  chfacfscmulgsum  22796  chfacfpmmulfsupp  22799  chfacfpmmulgsum  22800  cpmidpmatlem3  22808  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  cayhamlem4  22824  xpstopnlem2  23747  fcfval  23969  tsmsxplem1  24089  tsmsxplem2  24090  tusval  24202  xpsdsfn  24314  xpsxmet  24317  xpsdsval  24318  xpsmet  24319  tmsval  24418  met1stc  24458  metuval  24486  cnmpopc  24871  pi1val  24986  pi1addf  24996  pi1addval  24997  pi1grplem  24998  rrxnm  25341  rrxcph  25342  rrxmval  25355  mbfmulc2  25614  mbfmul  25677  itg2mulclem  25697  ibladd  25772  itgadd  25776  itgabs  25786  bddmulibl  25790  dvmulf  25896  dvcmulf  25898  dvmptmul  25915  cmvth  25945  dvlip  25948  ftc1lem4  25996  mdegmullem  26033  coe1mul3  26054  r1pval  26113  plyco  26196  dgrcolem1  26229  elqaalem3  26279  taylpfval  26322  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  advlogexp  26614  logtayl  26619  logccv  26622  dvcxp1  26699  dvcncxp1  26702  logbmpt  26748  logbfval  26750  relogbf  26751  dvatan  26895  cxp2lim  26937  cxploglim2  26939  lgamgulmlem2  26990  lgamgulm2  26996  lgamcvglem  27000  lgamf  27002  basellem7  27047  basellem8  27048  basellem9  27049  fsumdvdscom  27145  logexprlim  27186  dchrfi  27216  gausslemma2dlem2  27328  gausslemma2dlem3  27329  2lgslem1b  27353  chtppilimlem2  27435  chebbnd2  27438  chto1lb  27439  chpchtlim  27440  chpo1ub  27441  vmadivsum  27443  dchrisum0lem3  27480  mudivsum  27491  logdivsum  27494  log2sumbnd  27505  selberglem1  27506  selberg2lem  27511  selberg2  27512  selbergr  27529  negsval  27974  wlkp1  29607  cyclnumvtx  29728  wwlksnextsurj  29828  wwlksnextbij  29830  clwlkclwwlklem2a1  29919  clwlkclwwlkf1  29937  eupth2eucrct  30144  frgrncvvdeq  30236  numclwlk2lem2fv  30305  numclwwlk2lem3  30307  ofoprabco  32588  fsuppcurry1  32648  fsuppcurry2  32649  offinsupp1  32650  ressprs  32890  resspos  32892  mntoval  32908  mgcoval  32912  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  lmodvslmhm  32990  gsumwrd2dccat  33007  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  archirngz  33133  archiabllem2a  33138  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnsubrunlem2  33189  rlocval  33200  fracval  33244  quslmod  33319  quslmhm  33320  quslvec  33321  qustriv  33325  qustrivr  33326  unitprodclb  33350  nsgmgc  33373  nsgqusf1olem1  33374  nsgqusf1olem2  33375  nsgqusf1olem3  33376  lmhmqusker  33378  rhmquskerlem  33386  elrspunidl  33389  qsidomlem1  33413  qsidomlem2  33414  opprqusbas  33449  opprqusplusg  33450  opprqusmulr  33452  opprqus1r  33453  qsdrngilem  33455  qsdrngi  33456  rprmdvdsprod  33495  1arithidomlem1  33496  1arithidomlem2  33497  1arithidom  33498  1arithufdlem3  33507  dfufd2lem  33510  zringfrac  33515  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  ply1gsumz  33554  r1plmhm  33565  resssra  33573  ply1degltdimlem  33608  ply1degltdim  33609  qusdimsum  33614  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  lactlmhm  33620  fldgenfldext  33655  evls1fldgencl  33657  fldextrspunlsplem  33660  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  algextdeglem4  33700  algextdeglem6  33702  algextdeglem7  33703  submateq  33786  lmatcl  33793  mdetpmtr1  33800  madjusmdetlem1  33804  madjusmdetlem3  33806  qqhvval  33960  esumfzf  34046  esumpfinvallem  34051  esumpmono  34056  esummulc1  34058  esumcvg  34063  esumgect  34067  ofcval  34076  omssubadd  34278  sitgfval  34319  sitmcl  34329  sseqfv2  34372  cndprobval  34411  ballotlemfval  34468  ballotlemsv  34488  ballotlemsf1o  34492  ofcccat  34521  signsplypnf  34528  signsply0  34529  signstfval  34542  signshf  34566  reprpmtf1o  34604  reprdifc  34605  logdivsqrle  34628  hgt750lemg  34632  hgt750lema  34635  lpadval  34654  cvmliftlem8  35260  cvmliftphtlem  35285  fmla1  35355  gonarlem  35362  sategoelfvb  35387  mrsubval  35477  ellcsrspsn  35609  r1peuqusdeg1  35611  fwddifval  36126  knoppcnlem1  36457  knoppcnlem6  36462  unbdqndv2lem2  36474  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem19  37609  poimirlem22  37612  poimirlem23  37613  broucube  37624  dvtan  37640  itg2addnc  37644  ibladdnc  37647  itgaddnc  37650  itgmulc2nclem2  37657  itgmulc2nc  37658  itgabsnc  37659  ftc1cnnclem  37661  ftc1anclem3  37665  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  dvasin  37674  dvacos  37675  dvreasin  37676  dvreacos  37677  areacirclem1  37678  areacirc  37683  fsumshftd  38916  hlrelat5N  39366  rhmzrhval  41930  aks6d1c1  42075  hashscontpow  42081  aks6d1c4  42083  aks6d1c2lem3  42085  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5lem0  42094  aks6d1c5lem3  42096  aks6d1c5lem2  42097  aks6d1c5  42098  sticksstones3  42107  sticksstones8  42112  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem1  42129  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6isolem3  42135  aks6d1c6lem5  42136  aks6d1c7lem2  42140  unitscyglem1  42154  readvrec2  42351  readvrec  42352  readvcot  42354  frlmfzolen  42473  frlmfzoccat  42475  frlmvscadiccat  42476  evlscl  42528  evlsval3  42529  evlsvval  42530  evlsvvval  42533  evlsbagval  42536  evlsexpval  42537  evlsaddval  42538  evlsmulval  42539  evlsevl  42541  evlcl  42542  evladdval  42545  evlmulval  42546  selvcl  42553  evlselv  42557  fsuppind  42560  mhpind  42564  mhphflem  42566  prjspner  42589  prjspnvs  42590  prjspnfv01  42594  prjspner01  42595  prjspner1  42596  0prjspnrel  42597  prjcrv0  42603  mzpclall  42697  mzpsubst  42718  eldioph2  42732  rabdiophlem2  42772  irrapxlem1  42792  mzpcong  42943  mendlmod  43160  naddcnff  43333  relexpmulnn  43680  iunrelexpuztr  43690  mnringvald  44185  mnringmulrvald  44199  radcnvrat  44286  hashnzfzclim  44294  lhe4.4ex1a  44301  expgrowthi  44305  expgrowth  44307  bccval  44310  binomcxplemrat  44322  binomcxplemfrat  44323  binomcxplemradcnv  44324  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  unirnmap  45180  unirnmapsn  45186  ssmapsn  45188  iocopn  45497  icoopn  45502  divcnvg  45604  sumnnodd  45607  climsubmpt  45637  dvsinax  45890  fperdvper  45896  dvdivf  45899  dvnprodlem1  45923  itgsincmulx  45951  stoweidlem59  46036  etransclem4  46215  etransclem13  46224  etransclem25  46236  etransclem48  46259  rrxtopnfi  46264  sge0tsms  46357  elhoi  46519  ovnval2  46522  ovnval2b  46529  ovncvrrp  46541  ovn0lem  46542  ovncl  46544  ovnome  46550  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvle  46577  ovnlecvr2  46587  ovncvr2  46588  ovnsubadd2lem  46622  ovnovollem1  46633  vonvolmbl  46638  iunhoiioolem  46652  vonioolem1  46657  vonioolem2  46658  vonicclem2  46661  smfresal  46765  smfres  46767  smfmullem4  46771  smfco  46779  adddmmbl  46810  muldmmbl  46812  fmtno  47491  isubgruhgr  47829  grtriprop  47901  grtriclwlk3  47905  gpgvtx  47995  gpgiedg  47996  intopval  48125  clintopval  48127  rngchomALTV  48191  funcringcsetcALTV2lem5  48217  ringchomALTV  48225  funcringcsetclem5ALTV  48240  srhmsubcALTVlem2  48247  srhmsubcALTV  48248  fldhmsubcALTV  48256  zlmodzxzscm  48280  zlmodzxzadd  48281  rmsupp0  48291  domnmsuppn0  48292  rmsuppss  48293  ply1mulgsumlem3  48312  ply1mulgsumlem4  48313  ply1mulgsum  48314  dmatALTval  48324  lincop  48332  lincval  48333  linc1  48349  lincresunit3lem1  48403  fdivmpt  48468  fdivmptfv  48473  refdivmptfv  48474  digval  48526  2arymptfv  48578  2arymaptfo  48582  itcovalpclem1  48598  itcovalt2lem1  48603  ackvalsuc1mpt  48606  ackval1  48609  ackval2  48610  ackval3  48611  ackval42  48624  line2xlem  48681  upfval2  49060  swapfval  49127  tposcurf1  49158  tposcurf2val  49160  fucofvalg  49177  fuco112x  49191  fuco23  49200  fucoid  49207  fucocolem4  49215  prcofvalg  49235  prcof1  49246  lanval  49442  ranval  49443