Theorem ovexd 7393

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3439  (class class class)co 7358

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 2707  ax-nul 5250

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 2714  df-cleq 2727  df-clel 2810  df-ne 2932  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-sn 4580  df-pr 4582  df-uni 4863  df-iota 6447  df-fv 6499  df-ov 7361

This theorem is referenced by:  caofidlcan  7660  caofass  7662  caofdi  7664  caofdir  7665  caonncan  7666  suppofssd  8145  mapsnend  8975  snmapen  8977  pw2eng  9013  mapen  9071  mapxpen  9073  mapunen  9076  mapdom2  9078  cantnfcl  9578  cantnfle  9582  cantnflt  9583  cantnflt2  9584  cantnfp1lem2  9590  cantnfp1lem3  9591  cantnflem1b  9597  cantnflem1d  9599  cantnflem1  9600  cnfcomlem  9610  cnfcom  9611  cnfcom2lem  9612  cnfcom3lem  9614  fzen  13459  seqf1o  13968  wrdexg  14449  wrdnval  14470  pfxval  14599  pfxswrd  14631  splval  14676  ofccat  14894  climshftlem  15499  climshft  15501  climshft2  15507  caucvgr  15601  fsumrev  15704  hashdvds  16704  setsabs  17108  ressress  17176  firest  17354  prdsvscafval  17402  qusval  17465  xpsbas  17495  xpsadd  17497  xpsmul  17498  xpssca  17499  xpsvsca  17500  xpsless  17501  xpsle  17502  homfval  17617  comfval  17625  cicfval  17723  rescabs  17759  rescabs2  17760  resscat  17778  funcres2c  17829  ressffth  17866  fucbas  17889  fuccoval  17892  setchom  18006  catchom  18029  catcco  18031  estrchom  18052  funcestrcsetclem5  18069  funcsetcestrclem5  18084  evlf2val  18144  curf11  18151  curf12  18152  curf2val  18155  uncfval  18159  diagval  18165  hof2  18182  yonval  18186  resspos  18354  gsumval2a  18612  gsumval2  18613  mndpsuppss  18692  gsumwspan  18773  efmnd  18797  ghmqusnsglem1  19211  ghmqusnsglem2  19212  ghmqusnsg  19213  ghmquskerlem1  19214  ghmquskerco  19215  ghmquskerlem2  19216  ghmquskerlem3  19217  ghmqusker  19218  orbstafun  19242  orbstaval  19243  symgval  19302  psgnvalii  19440  lsmhash  19636  frgpupval  19705  qusabl  19796  gsumval3  19838  gsumreidx  19848  gsumzaddlem  19852  gsummptshft  19867  telgsumfzslem  19919  telgsumfz  19921  telgsumfz0  19923  dpjval  19989  prdsrngd  20113  srgbinomlem3  20165  srgbinomlem4  20166  mulgass3  20291  rngcval  20553  rnghmsscmap2  20564  rnghmsscmap  20565  funcrngcsetc  20575  ringcval  20582  rhmsscmap2  20593  rhmsscmap  20594  funcringcsetc  20609  srhmsubclem3  20614  srhmsubc  20615  fldhmsubc  20720  lcomfsupp  20855  rmodislmodlem  20882  rmodislmod  20883  sraval  21129  srasca  21134  crngridl  21237  quscrng  21240  rhmqusnsg  21242  pzriprnglem11  21448  znval  21492  znzrhfo  21504  znunithash  21521  cygznlem2  21525  frobrhm  21532  pjfval  21663  pjpm  21665  frlmgsum  21729  frlmipval  21736  frlmphllem  21737  frlmphl  21738  frlmsslsp  21753  frlmup1  21755  gsumbagdiaglem  21888  psrass1lem  21890  rhmpsrlem1  21898  psrass1  21921  psrdi  21922  psrdir  21923  psrass23l  21924  psrascl  21936  mplval  21946  mplsubglem  21956  mplsubrglem  21961  mplmonmul  21993  mplcoe1  21994  opsrval  22003  psrbagev1  22034  psrbagev2  22035  evlslem6  22038  evlslem1  22039  evlsval  22043  evlsval3  22046  evlsvval  22047  evlsvvval  22050  evlcl  22059  evladdval  22060  evlmulval  22061  mpfconst  22066  mpff  22069  mpfaddcl  22070  mpfmulcl  22071  mpfind  22072  mhpmulcl  22094  mhpaddcl  22096  psdcoef  22105  psdmplcl  22107  psdadd  22108  ply1lss  22139  gsumply1subr  22176  coe1add  22208  coe1tm  22217  coe1tmmul  22221  cply1mul  22242  ply1coe  22244  evl1expd  22291  pf1mpf  22298  pf1ind  22301  mhmcompl  22326  mhmcoaddmpl  22327  rhmmpl  22329  rhmply1vsca  22334  mamufv  22340  mamuass  22348  mamuvs1  22351  mamuvs2  22352  matgsum  22383  dmatmul  22443  scmatval  22450  scmatrhmval  22473  mvmulfv  22490  mavmulfv  22492  mavmulass  22495  marrepeval  22509  marepveval  22514  submaeval  22528  mdetrsca  22549  mdetunilem9  22566  mdetuni0  22567  gsummatr01lem3  22603  gsummatr01lem4  22604  gsummatr01  22605  smadiadetlem3  22614  cramerlem1  22633  mat2pmatmul  22677  m2cpminvid  22699  decpmatfsupp  22715  decpmatmullem  22717  decpmatmul  22718  decpmatmulsumfsupp  22719  pmatcollpw1lem1  22720  pmatcollpw3fi1lem1  22732  pmatcollpwscmatlem2  22736  pm2mpfval  22742  pm2mpf  22744  mply1topmatcllem  22749  mp2pm2mplem3  22754  mp2pm2mplem4  22755  pm2mpmhmlem1  22764  pm2mpmhmlem2  22765  pm2mp  22771  chfacfscmulfsupp  22805  chfacfscmulgsum  22806  chfacfpmmulfsupp  22809  chfacfpmmulgsum  22810  cpmidpmatlem3  22818  cpmadugsumlemB  22820  cpmadugsumlemC  22821  cpmadugsumlemF  22822  cayhamlem4  22834  xpstopnlem2  23757  fcfval  23979  tsmsxplem1  24099  tsmsxplem2  24100  tusval  24211  xpsdsfn  24323  xpsxmet  24326  xpsdsval  24327  xpsmet  24328  tmsval  24427  met1stc  24467  metuval  24495  cnmpopc  24880  pi1val  24995  pi1addf  25005  pi1addval  25006  pi1grplem  25007  rrxnm  25349  rrxcph  25350  rrxmval  25363  mbfmulc2  25622  mbfmul  25685  itg2mulclem  25705  ibladd  25780  itgadd  25784  itgabs  25794  bddmulibl  25798  dvmulf  25904  dvcmulf  25906  dvmptmul  25923  cmvth  25953  dvlip  25956  ftc1lem4  26004  mdegmullem  26041  coe1mul3  26062  r1pval  26121  plyco  26204  dgrcolem1  26237  elqaalem3  26287  taylpfval  26330  taylthlem2  26340  taylthlem2OLD  26341  pserdvlem2  26396  advlogexp  26622  logtayl  26627  logccv  26630  dvcxp1  26707  dvcncxp1  26710  logbmpt  26756  logbfval  26758  relogbf  26759  dvatan  26903  cxp2lim  26945  cxploglim2  26947  lgamgulmlem2  26998  lgamgulm2  27004  lgamcvglem  27008  lgamf  27010  basellem7  27055  basellem8  27056  basellem9  27057  fsumdvdscom  27153  logexprlim  27194  dchrfi  27224  gausslemma2dlem2  27336  gausslemma2dlem3  27337  2lgslem1b  27361  chtppilimlem2  27443  chebbnd2  27446  chto1lb  27447  chpchtlim  27448  chpo1ub  27449  vmadivsum  27451  dchrisum0lem3  27488  mudivsum  27499  logdivsum  27502  log2sumbnd  27513  selberglem1  27514  selberg2lem  27519  selberg2  27520  selbergr  27537  negsval  28005  wlkp1  29734  cyclnumvtx  29854  wwlksnextsurj  29954  wwlksnextbij  29956  clwlkclwwlklem2a1  30048  clwlkclwwlkf1  30066  eupth2eucrct  30273  frgrncvvdeq  30365  numclwlk2lem2fv  30434  numclwwlk2lem3  30436  ofoprabco  32722  fsuppcurry1  32782  fsuppcurry2  32783  offinsupp1  32784  ressprs  33027  mntoval  33043  mgcoval  33047  mndlactf1  33087  mndlactfo  33088  mndractf1  33089  mndractfo  33090  mndlactf1o  33091  mndractf1o  33092  lmodvslmhm  33112  gsummulsubdishift2  33131  gsumwrd2dccat  33139  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  conjga  33231  cntrval2  33232  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  fxpsdrg  33236  archirngz  33250  archiabllem2a  33255  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnsubrunlem2  33309  rlocval  33320  fracval  33365  quslmod  33418  quslmhm  33419  quslvec  33420  qustriv  33424  qustrivr  33425  unitprodclb  33449  nsgmgc  33472  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475  lmhmqusker  33477  rhmquskerlem  33485  elrspunidl  33488  qsidomlem1  33512  qsidomlem2  33513  opprqusbas  33548  opprqusplusg  33549  opprqusmulr  33551  opprqus1r  33552  qsdrngilem  33554  qsdrngi  33555  rprmdvdsprod  33594  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  1arithufdlem3  33606  dfufd2lem  33609  zringfrac  33614  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ply1gsumz  33659  r1plmhm  33670  mplvrpmrhm  33691  splyval  33696  vietadeg1  33713  resssra  33722  ply1degltdimlem  33758  ply1degltdim  33759  qusdimsum  33764  fedgmullem1  33765  fedgmullem2  33766  fedgmul  33767  lactlmhm  33770  fldgenfldext  33804  evls1fldgencl  33806  fldextrspunlsplem  33809  fldextrspundgdvdslem  33816  fldextrspundgdvds  33817  extdgfialglem1  33828  extdgfialglem2  33829  extdgfialg  33830  algextdeglem4  33856  algextdeglem6  33858  algextdeglem7  33859  submateq  33945  lmatcl  33952  mdetpmtr1  33959  madjusmdetlem1  33963  madjusmdetlem3  33965  qqhvval  34119  esumfzf  34205  esumpfinvallem  34210  esumpmono  34215  esummulc1  34217  esumcvg  34222  esumgect  34226  ofcval  34235  omssubadd  34436  sitgfval  34477  sitmcl  34487  sseqfv2  34530  cndprobval  34569  ballotlemfval  34626  ballotlemsv  34646  ballotlemsf1o  34650  ofcccat  34679  signsplypnf  34686  signsply0  34687  signstfval  34700  signshf  34724  reprpmtf1o  34762  reprdifc  34763  logdivsqrle  34786  hgt750lemg  34790  hgt750lema  34793  lpadval  34812  cvmliftlem8  35465  cvmliftphtlem  35490  fmla1  35560  gonarlem  35567  sategoelfvb  35592  mrsubval  35682  ellcsrspsn  35814  r1peuqusdeg1  35816  fwddifval  36335  knoppcnlem1  36666  knoppcnlem6  36671  unbdqndv2lem2  36683  poimirlem1  37791  poimirlem2  37792  poimirlem3  37793  poimirlem5  37795  poimirlem6  37796  poimirlem7  37797  poimirlem10  37800  poimirlem11  37801  poimirlem12  37802  poimirlem16  37806  poimirlem19  37809  poimirlem22  37812  poimirlem23  37813  broucube  37824  dvtan  37840  itg2addnc  37844  ibladdnc  37847  itgaddnc  37850  itgmulc2nclem2  37857  itgmulc2nc  37858  itgabsnc  37859  ftc1cnnclem  37861  ftc1anclem3  37865  ftc1anclem6  37868  ftc1anclem7  37869  ftc1anclem8  37870  dvasin  37874  dvacos  37875  dvreasin  37876  dvreacos  37877  areacirclem1  37878  areacirc  37883  fsumshftd  39247  hlrelat5N  39696  rhmzrhval  42260  aks6d1c1  42405  hashscontpow  42411  aks6d1c4  42413  aks6d1c2lem3  42415  aks6d1c2lem4  42416  aks6d1c2  42419  aks6d1c5lem0  42424  aks6d1c5lem3  42426  aks6d1c5lem2  42427  aks6d1c5  42428  sticksstones3  42437  sticksstones8  42442  sticksstones10  42444  sticksstones12a  42446  sticksstones12  42447  aks6d1c6lem1  42459  aks6d1c6lem2  42460  aks6d1c6lem3  42461  aks6d1c6lem4  42462  aks6d1c6isolem1  42463  aks6d1c6isolem2  42464  aks6d1c6isolem3  42465  aks6d1c6lem5  42466  aks6d1c7lem2  42470  unitscyglem1  42484  readvrec2  42653  readvrec  42654  readvcot  42656  frlmfzolen  42795  frlmfzoccat  42797  frlmvscadiccat  42798  evlscl  42846  evlsbagval  42849  evlsexpval  42850  evlsaddval  42851  evlsmulval  42852  evlsevl  42854  selvcl  42863  evlselv  42867  fsuppind  42870  mhpind  42874  mhphflem  42876  prjspner  42899  prjspnvs  42900  prjspnfv01  42904  prjspner01  42905  prjspner1  42906  0prjspnrel  42907  prjcrv0  42913  mzpclall  43006  mzpsubst  43027  eldioph2  43041  rabdiophlem2  43081  irrapxlem1  43101  mzpcong  43251  mendlmod  43468  naddcnff  43641  relexpmulnn  43987  iunrelexpuztr  43997  mnringvald  44491  mnringmulrvald  44505  radcnvrat  44592  hashnzfzclim  44600  lhe4.4ex1a  44607  expgrowthi  44611  expgrowth  44613  bccval  44616  binomcxplemrat  44628  binomcxplemfrat  44629  binomcxplemradcnv  44630  binomcxplemdvbinom  44631  binomcxplemdvsum  44633  binomcxplemnotnn0  44634  unirnmap  45489  unirnmapsn  45495  ssmapsn  45497  iocopn  45803  icoopn  45808  divcnvg  45910  sumnnodd  45913  climsubmpt  45941  dvsinax  46194  fperdvper  46200  dvdivf  46203  dvnprodlem1  46227  itgsincmulx  46255  stoweidlem59  46340  etransclem4  46519  etransclem13  46528  etransclem25  46540  etransclem48  46563  rrxtopnfi  46568  sge0tsms  46661  elhoi  46823  ovnval2  46826  ovnval2b  46833  ovncvrrp  46845  ovn0lem  46846  ovncl  46848  ovnome  46854  hoidmvlelem2  46877  hoidmvlelem3  46878  hoidmvle  46881  ovnlecvr2  46891  ovncvr2  46892  ovnsubadd2lem  46926  ovnovollem1  46937  vonvolmbl  46942  iunhoiioolem  46956  vonioolem1  46961  vonioolem2  46962  vonicclem2  46965  smfresal  47069  smfres  47071  smfmullem4  47075  smfco  47083  adddmmbl  47114  muldmmbl  47116  chnsuslle  47162  nthrucw  47167  sinnpoly  47174  fmtno  47812  isubgruhgr  48151  grtriprop  48224  grtriclwlk3  48228  gpgvtx  48326  gpgiedg  48327  intopval  48485  clintopval  48487  rngchomALTV  48551  funcringcsetcALTV2lem5  48577  ringchomALTV  48585  funcringcsetclem5ALTV  48600  srhmsubcALTVlem2  48607  srhmsubcALTV  48608  fldhmsubcALTV  48616  zlmodzxzscm  48640  zlmodzxzadd  48641  rmsupp0  48651  domnmsuppn0  48652  rmsuppss  48653  ply1mulgsumlem3  48671  ply1mulgsumlem4  48672  ply1mulgsum  48673  dmatALTval  48683  lincop  48691  lincval  48692  linc1  48708  lincresunit3lem1  48762  fdivmpt  48823  fdivmptfv  48828  refdivmptfv  48829  digval  48881  2arymptfv  48933  2arymaptfo  48937  itcovalpclem1  48953  itcovalt2lem1  48958  ackvalsuc1mpt  48961  ackval1  48964  ackval2  48965  ackval3  48966  ackval42  48979  line2xlem  49036  upfval2  49459  swapfval  49544  tposcurf1  49581  tposcurf2val  49583  fucofvalg  49600  fuco112x  49614  fuco23  49623  fucoid  49630  fucocolem4  49638  prcofvalg  49658  prcof1  49670  opf2fval  49687  lanval  49901  ranval  49902