Theorem ovexd 7405

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

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

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 6453  df-fv 6508  df-ov 7373

This theorem is referenced by:  caofidlcan  7672  caofass  7674  caofdi  7676  caofdir  7677  caonncan  7678  suppofssd  8160  mapsnend  8985  snmapen  8987  pw2eng  9025  mapen  9083  mapxpen  9085  mapunen  9088  mapdom2  9090  cantnfcl  9599  cantnfle  9603  cantnflt  9604  cantnflt2  9605  cantnfp1lem2  9611  cantnfp1lem3  9612  cantnflem1b  9618  cantnflem1d  9620  cantnflem1  9621  cnfcomlem  9631  cnfcom  9632  cnfcom2lem  9633  cnfcom3lem  9635  fzen  13481  seqf1o  13987  wrdexg  14468  wrdnval  14489  pfxval  14617  pfxswrd  14649  splval  14694  cshwsexaOLD  14768  ofccat  14913  climshftlem  15518  climshft  15520  climshft2  15526  caucvgr  15620  fsumrev  15723  hashdvds  16723  setsabs  17127  ressress  17195  firest  17373  prdsvscafval  17421  qusval  17483  xpsbas  17513  xpsadd  17515  xpsmul  17516  xpssca  17517  xpsvsca  17518  xpsless  17519  xpsle  17520  homfval  17635  comfval  17643  cicfval  17741  rescabs  17777  rescabs2  17778  resscat  17796  funcres2c  17847  ressffth  17884  fucbas  17907  fuccoval  17910  setchom  18024  catchom  18047  catcco  18049  estrchom  18070  funcestrcsetclem5  18087  funcsetcestrclem5  18102  evlf2val  18162  curf11  18169  curf12  18170  curf2val  18173  uncfval  18177  diagval  18183  hof2  18200  yonval  18204  resspos  18372  gsumval2a  18596  gsumval2  18597  mndpsuppss  18676  gsumwspan  18757  efmnd  18781  ghmqusnsglem1  19196  ghmqusnsglem2  19197  ghmqusnsg  19198  ghmquskerlem1  19199  ghmquskerco  19200  ghmquskerlem2  19201  ghmquskerlem3  19202  ghmqusker  19203  orbstafun  19227  orbstaval  19228  symgval  19287  psgnvalii  19425  lsmhash  19621  frgpupval  19690  qusabl  19781  gsumval3  19823  gsumreidx  19833  gsumzaddlem  19837  gsummptshft  19852  telgsumfzslem  19904  telgsumfz  19906  telgsumfz0  19908  dpjval  19974  prdsrngd  20098  srgbinomlem3  20150  srgbinomlem4  20151  mulgass3  20275  rngcval  20540  rnghmsscmap2  20551  rnghmsscmap  20552  funcrngcsetc  20562  ringcval  20569  rhmsscmap2  20580  rhmsscmap  20581  funcringcsetc  20596  srhmsubclem3  20601  srhmsubc  20602  fldhmsubc  20707  lcomfsupp  20842  rmodislmodlem  20869  rmodislmod  20870  sraval  21116  srasca  21121  crngridl  21224  quscrng  21227  rhmqusnsg  21229  pzriprnglem11  21435  znval  21479  znzrhfo  21491  znunithash  21508  cygznlem2  21512  frobrhm  21519  pjfval  21650  pjpm  21652  frlmgsum  21716  frlmipval  21723  frlmphllem  21724  frlmphl  21725  frlmsslsp  21740  frlmup1  21742  gsumbagdiaglem  21874  psrass1lem  21876  rhmpsrlem1  21884  psrass1  21908  psrdi  21909  psrdir  21910  psrass23l  21911  psrascl  21923  mplval  21933  mplsubglem  21943  mplsubrglem  21948  mplmonmul  21978  mplcoe1  21979  opsrval  21988  psrbagev1  22019  psrbagev2  22020  evlslem6  22023  evlslem1  22024  evlsval  22028  mpfconst  22043  mpff  22046  mpfaddcl  22047  mpfmulcl  22048  mpfind  22049  mhpmulcl  22071  mhpaddcl  22073  psdcoef  22082  psdmplcl  22084  psdadd  22085  ply1lss  22116  gsumply1subr  22153  coe1add  22185  coe1tm  22194  coe1tmmul  22198  cply1mul  22218  ply1coe  22220  evl1expd  22267  pf1mpf  22274  pf1ind  22277  mhmcompl  22302  mhmcoaddmpl  22303  rhmmpl  22305  rhmply1vsca  22310  mamufv  22316  mamuass  22324  mamuvs1  22327  mamuvs2  22328  matgsum  22359  dmatmul  22419  scmatval  22426  scmatrhmval  22449  mvmulfv  22466  mavmulfv  22468  mavmulass  22471  marrepeval  22485  marepveval  22490  submaeval  22504  mdetrsca  22525  mdetunilem9  22542  mdetuni0  22543  gsummatr01lem3  22579  gsummatr01lem4  22580  gsummatr01  22581  smadiadetlem3  22590  cramerlem1  22609  mat2pmatmul  22653  m2cpminvid  22675  decpmatfsupp  22691  decpmatmullem  22693  decpmatmul  22694  decpmatmulsumfsupp  22695  pmatcollpw1lem1  22696  pmatcollpw3fi1lem1  22708  pmatcollpwscmatlem2  22712  pm2mpfval  22718  pm2mpf  22720  mply1topmatcllem  22725  mp2pm2mplem3  22730  mp2pm2mplem4  22731  pm2mpmhmlem1  22740  pm2mpmhmlem2  22741  pm2mp  22747  chfacfscmulfsupp  22781  chfacfscmulgsum  22782  chfacfpmmulfsupp  22785  chfacfpmmulgsum  22786  cpmidpmatlem3  22794  cpmadugsumlemB  22796  cpmadugsumlemC  22797  cpmadugsumlemF  22798  cayhamlem4  22810  xpstopnlem2  23733  fcfval  23955  tsmsxplem1  24075  tsmsxplem2  24076  tusval  24188  xpsdsfn  24300  xpsxmet  24303  xpsdsval  24304  xpsmet  24305  tmsval  24404  met1stc  24444  metuval  24472  cnmpopc  24857  pi1val  24972  pi1addf  24982  pi1addval  24983  pi1grplem  24984  rrxnm  25326  rrxcph  25327  rrxmval  25340  mbfmulc2  25599  mbfmul  25662  itg2mulclem  25682  ibladd  25757  itgadd  25761  itgabs  25771  bddmulibl  25775  dvmulf  25881  dvcmulf  25883  dvmptmul  25900  cmvth  25930  dvlip  25933  ftc1lem4  25981  mdegmullem  26018  coe1mul3  26039  r1pval  26098  plyco  26181  dgrcolem1  26214  elqaalem3  26264  taylpfval  26307  taylthlem2  26317  taylthlem2OLD  26318  pserdvlem2  26373  advlogexp  26599  logtayl  26604  logccv  26607  dvcxp1  26684  dvcncxp1  26687  logbmpt  26733  logbfval  26735  relogbf  26736  dvatan  26880  cxp2lim  26922  cxploglim2  26924  lgamgulmlem2  26975  lgamgulm2  26981  lgamcvglem  26985  lgamf  26987  basellem7  27032  basellem8  27033  basellem9  27034  fsumdvdscom  27130  logexprlim  27171  dchrfi  27201  gausslemma2dlem2  27313  gausslemma2dlem3  27314  2lgslem1b  27338  chtppilimlem2  27420  chebbnd2  27423  chto1lb  27424  chpchtlim  27425  chpo1ub  27426  vmadivsum  27428  dchrisum0lem3  27465  mudivsum  27476  logdivsum  27479  log2sumbnd  27490  selberglem1  27491  selberg2lem  27496  selberg2  27497  selbergr  27514  negsval  27973  wlkp1  29662  cyclnumvtx  29782  wwlksnextsurj  29882  wwlksnextbij  29884  clwlkclwwlklem2a1  29973  clwlkclwwlkf1  29991  eupth2eucrct  30198  frgrncvvdeq  30290  numclwlk2lem2fv  30359  numclwwlk2lem3  30361  ofoprabco  32640  fsuppcurry1  32700  fsuppcurry2  32701  offinsupp1  32702  ressprs  32940  mntoval  32956  mgcoval  32960  mndlactf1  33012  mndlactfo  33013  mndractf1  33014  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  lmodvslmhm  33035  gsumwrd2dccat  33052  cycpmco2f1  33098  cycpmco2rn  33099  cycpmco2lem2  33101  cycpmco2lem3  33102  cycpmco2lem4  33103  cycpmco2lem5  33104  cycpmco2lem6  33105  cycpmco2  33107  conjga  33144  cntrval2  33145  fxpsubm  33146  archirngz  33160  archiabllem2a  33165  elrgspnlem1  33211  elrgspnlem2  33212  elrgspnsubrunlem2  33217  rlocval  33228  fracval  33272  quslmod  33324  quslmhm  33325  quslvec  33326  qustriv  33330  qustrivr  33331  unitprodclb  33355  nsgmgc  33378  nsgqusf1olem1  33379  nsgqusf1olem2  33380  nsgqusf1olem3  33381  lmhmqusker  33383  rhmquskerlem  33391  elrspunidl  33394  qsidomlem1  33418  qsidomlem2  33419  opprqusbas  33454  opprqusplusg  33455  opprqusmulr  33457  opprqus1r  33458  qsdrngilem  33460  qsdrngi  33461  rprmdvdsprod  33500  1arithidomlem1  33501  1arithidomlem2  33502  1arithidom  33503  1arithufdlem3  33512  dfufd2lem  33515  zringfrac  33520  evl1deg1  33540  evl1deg2  33541  evl1deg3  33542  ply1gsumz  33559  r1plmhm  33570  resssra  33578  ply1degltdimlem  33613  ply1degltdim  33614  qusdimsum  33619  fedgmullem1  33620  fedgmullem2  33621  fedgmul  33622  lactlmhm  33625  fldgenfldext  33658  evls1fldgencl  33660  fldextrspunlsplem  33663  fldextrspundgdvdslem  33670  fldextrspundgdvds  33671  algextdeglem4  33705  algextdeglem6  33707  algextdeglem7  33708  submateq  33794  lmatcl  33801  mdetpmtr1  33808  madjusmdetlem1  33812  madjusmdetlem3  33814  qqhvval  33968  esumfzf  34054  esumpfinvallem  34059  esumpmono  34064  esummulc1  34066  esumcvg  34071  esumgect  34075  ofcval  34084  omssubadd  34286  sitgfval  34327  sitmcl  34337  sseqfv2  34380  cndprobval  34419  ballotlemfval  34476  ballotlemsv  34496  ballotlemsf1o  34500  ofcccat  34529  signsplypnf  34536  signsply0  34537  signstfval  34550  signshf  34574  reprpmtf1o  34612  reprdifc  34613  logdivsqrle  34636  hgt750lemg  34640  hgt750lema  34643  lpadval  34662  cvmliftlem8  35274  cvmliftphtlem  35299  fmla1  35369  gonarlem  35376  sategoelfvb  35401  mrsubval  35491  ellcsrspsn  35623  r1peuqusdeg1  35625  fwddifval  36145  knoppcnlem1  36476  knoppcnlem6  36481  unbdqndv2lem2  36493  poimirlem1  37610  poimirlem2  37611  poimirlem3  37612  poimirlem5  37614  poimirlem6  37615  poimirlem7  37616  poimirlem10  37619  poimirlem11  37620  poimirlem12  37621  poimirlem16  37625  poimirlem19  37628  poimirlem22  37631  poimirlem23  37632  broucube  37643  dvtan  37659  itg2addnc  37663  ibladdnc  37666  itgaddnc  37669  itgmulc2nclem2  37676  itgmulc2nc  37677  itgabsnc  37678  ftc1cnnclem  37680  ftc1anclem3  37684  ftc1anclem6  37687  ftc1anclem7  37688  ftc1anclem8  37689  dvasin  37693  dvacos  37694  dvreasin  37695  dvreacos  37696  areacirclem1  37697  areacirc  37702  fsumshftd  38940  hlrelat5N  39390  rhmzrhval  41954  aks6d1c1  42099  hashscontpow  42105  aks6d1c4  42107  aks6d1c2lem3  42109  aks6d1c2lem4  42110  aks6d1c2  42113  aks6d1c5lem0  42118  aks6d1c5lem3  42120  aks6d1c5lem2  42121  aks6d1c5  42122  sticksstones3  42131  sticksstones8  42136  sticksstones10  42138  sticksstones12a  42140  sticksstones12  42141  aks6d1c6lem1  42153  aks6d1c6lem2  42154  aks6d1c6lem3  42155  aks6d1c6lem4  42156  aks6d1c6isolem1  42157  aks6d1c6isolem2  42158  aks6d1c6isolem3  42159  aks6d1c6lem5  42160  aks6d1c7lem2  42164  unitscyglem1  42178  readvrec2  42344  readvrec  42345  readvcot  42347  frlmfzolen  42486  frlmfzoccat  42488  frlmvscadiccat  42489  evlscl  42541  evlsval3  42542  evlsvval  42543  evlsvvval  42546  evlsbagval  42549  evlsexpval  42550  evlsaddval  42551  evlsmulval  42552  evlsevl  42554  evlcl  42555  evladdval  42558  evlmulval  42559  selvcl  42566  evlselv  42570  fsuppind  42573  mhpind  42577  mhphflem  42579  prjspner  42602  prjspnvs  42603  prjspnfv01  42607  prjspner01  42608  prjspner1  42609  0prjspnrel  42610  prjcrv0  42616  mzpclall  42710  mzpsubst  42731  eldioph2  42745  rabdiophlem2  42785  irrapxlem1  42805  mzpcong  42956  mendlmod  43173  naddcnff  43346  relexpmulnn  43693  iunrelexpuztr  43703  mnringvald  44197  mnringmulrvald  44211  radcnvrat  44298  hashnzfzclim  44306  lhe4.4ex1a  44313  expgrowthi  44317  expgrowth  44319  bccval  44322  binomcxplemrat  44334  binomcxplemfrat  44335  binomcxplemradcnv  44336  binomcxplemdvbinom  44337  binomcxplemdvsum  44339  binomcxplemnotnn0  44340  unirnmap  45197  unirnmapsn  45203  ssmapsn  45205  iocopn  45513  icoopn  45518  divcnvg  45620  sumnnodd  45623  climsubmpt  45653  dvsinax  45906  fperdvper  45912  dvdivf  45915  dvnprodlem1  45939  itgsincmulx  45967  stoweidlem59  46052  etransclem4  46231  etransclem13  46240  etransclem25  46252  etransclem48  46275  rrxtopnfi  46280  sge0tsms  46373  elhoi  46535  ovnval2  46538  ovnval2b  46545  ovncvrrp  46557  ovn0lem  46558  ovncl  46560  ovnome  46566  hoidmvlelem2  46589  hoidmvlelem3  46590  hoidmvle  46593  ovnlecvr2  46603  ovncvr2  46604  ovnsubadd2lem  46638  ovnovollem1  46649  vonvolmbl  46654  iunhoiioolem  46668  vonioolem1  46673  vonioolem2  46674  vonicclem2  46677  smfresal  46781  smfres  46783  smfmullem4  46787  smfco  46795  adddmmbl  46826  muldmmbl  46828  sinnpoly  46887  fmtno  47525  isubgruhgr  47863  grtriprop  47935  grtriclwlk3  47939  gpgvtx  48029  gpgiedg  48030  intopval  48185  clintopval  48187  rngchomALTV  48251  funcringcsetcALTV2lem5  48277  ringchomALTV  48285  funcringcsetclem5ALTV  48300  srhmsubcALTVlem2  48307  srhmsubcALTV  48308  fldhmsubcALTV  48316  zlmodzxzscm  48340  zlmodzxzadd  48341  rmsupp0  48351  domnmsuppn0  48352  rmsuppss  48353  ply1mulgsumlem3  48372  ply1mulgsumlem4  48373  ply1mulgsum  48374  dmatALTval  48384  lincop  48392  lincval  48393  linc1  48409  lincresunit3lem1  48463  fdivmpt  48524  fdivmptfv  48529  refdivmptfv  48530  digval  48582  2arymptfv  48634  2arymaptfo  48638  itcovalpclem1  48654  itcovalt2lem1  48659  ackvalsuc1mpt  48662  ackval1  48665  ackval2  48666  ackval3  48667  ackval42  48680  line2xlem  48737  upfval2  49161  swapfval  49246  tposcurf1  49283  tposcurf2val  49285  fucofvalg  49302  fuco112x  49316  fuco23  49325  fucoid  49332  fucocolem4  49340  prcofvalg  49360  prcof1  49372  opf2fval  49389  lanval  49603  ranval  49604