Theorem ovexd 7483

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  caofass  7752  caofdi  7754  caofdir  7755  caonncan  7756  suppofssd  8244  mapsnend  9101  snmapen  9103  pw2eng  9144  mapen  9207  mapxpen  9209  mapunen  9212  mapdom2  9214  cantnfcl  9736  cantnfle  9740  cantnflt  9741  cantnflt2  9742  cantnfp1lem2  9748  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1d  9757  cantnflem1  9758  cnfcomlem  9768  cnfcom  9769  cnfcom2lem  9770  cnfcom3lem  9772  fzen  13601  seqf1o  14094  wrdexg  14572  wrdnval  14593  pfxval  14721  pfxswrd  14754  splval  14799  cshwsexaOLD  14873  ofccat  15018  climshftlem  15620  climshft  15622  climshft2  15628  caucvgr  15724  fsumrev  15827  hashdvds  16822  setsabs  17226  ressress  17307  firest  17492  prdsvscafval  17540  qusval  17602  xpsbas  17632  xpsadd  17634  xpsmul  17635  xpssca  17636  xpsvsca  17637  xpsless  17638  xpsle  17639  homfval  17750  comfval  17758  cicfval  17858  rescabs  17896  rescabsOLD  17897  rescabs2  17898  resscat  17916  funcres2c  17968  ressffth  18005  fucbas  18029  fuccoval  18033  setchom  18147  catchom  18170  catcco  18172  estrchom  18195  funcestrcsetclem5  18213  funcsetcestrclem5  18228  evlf2val  18289  curf11  18296  curf12  18297  curf2val  18300  uncfval  18304  diagval  18310  hof2  18327  yonval  18331  gsumval2a  18723  gsumval2  18724  gsumwspan  18881  efmnd  18905  ghmqusnsglem1  19320  ghmqusnsglem2  19321  ghmqusnsg  19322  ghmquskerlem1  19323  ghmquskerco  19324  ghmquskerlem2  19325  ghmquskerlem3  19326  ghmqusker  19327  orbstafun  19351  orbstaval  19352  symgval  19412  psgnvalii  19551  lsmhash  19747  frgpupval  19816  qusabl  19907  gsumval3  19949  gsumreidx  19959  gsumzaddlem  19963  gsummptshft  19978  telgsumfzslem  20030  telgsumfz  20032  telgsumfz0  20034  dpjval  20100  prdsrngd  20203  srgbinomlem3  20255  srgbinomlem4  20256  mulgass3  20379  rngcval  20640  rnghmsscmap2  20651  rnghmsscmap  20652  funcrngcsetc  20662  ringcval  20669  rhmsscmap2  20680  rhmsscmap  20681  funcringcsetc  20696  srhmsubclem3  20701  srhmsubc  20702  fldhmsubc  20808  lcomfsupp  20922  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  sraval  21197  srasca  21206  srascaOLD  21207  crngridl  21313  quscrng  21316  rhmqusnsg  21318  pzriprnglem11  21525  znval  21573  znzrhfo  21589  znunithash  21606  cygznlem2  21610  frobrhm  21617  pjfval  21749  pjpm  21751  frlmgsum  21815  frlmipval  21822  frlmphllem  21823  frlmphl  21824  frlmsslsp  21839  frlmup1  21841  gsumbagdiaglem  21973  psrass1lem  21975  rhmpsrlem1  21983  psrass1  22007  psrdi  22008  psrdir  22009  psrass23l  22010  psrascl  22022  mplval  22032  mplsubglem  22042  mplsubrglem  22047  mplmonmul  22077  mplcoe1  22078  opsrval  22087  psrbagev1  22124  psrbagev2  22125  evlslem6  22128  evlslem1  22129  evlsval  22133  mpfconst  22148  mpff  22151  mpfaddcl  22152  mpfmulcl  22153  mpfind  22154  mhpmulcl  22176  mhpaddcl  22178  psdcoef  22187  psdmplcl  22189  psdadd  22190  ply1lss  22219  gsumply1subr  22256  coe1add  22288  coe1tm  22297  coe1tmmul  22301  cply1mul  22321  ply1coe  22323  evl1expd  22370  pf1mpf  22377  pf1ind  22380  mhmcompl  22405  mhmcoaddmpl  22406  rhmmpl  22408  rhmply1vsca  22413  mamufv  22419  mamuass  22427  mamuvs1  22430  mamuvs2  22431  matgsum  22464  dmatmul  22524  scmatval  22531  scmatrhmval  22554  mvmulfv  22571  mavmulfv  22573  mavmulass  22576  marrepeval  22590  marepveval  22595  submaeval  22609  mdetrsca  22630  mdetunilem9  22647  mdetuni0  22648  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  smadiadetlem3  22695  cramerlem1  22714  mat2pmatmul  22758  m2cpminvid  22780  decpmatfsupp  22796  decpmatmullem  22798  decpmatmul  22799  decpmatmulsumfsupp  22800  pmatcollpw1lem1  22801  pmatcollpw3fi1lem1  22813  pmatcollpwscmatlem2  22817  pm2mpfval  22823  pm2mpf  22825  mply1topmatcllem  22830  mp2pm2mplem3  22835  mp2pm2mplem4  22836  pm2mpmhmlem1  22845  pm2mpmhmlem2  22846  pm2mp  22852  chfacfscmulfsupp  22886  chfacfscmulgsum  22887  chfacfpmmulfsupp  22890  chfacfpmmulgsum  22891  cpmidpmatlem3  22899  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  cayhamlem4  22915  xpstopnlem2  23840  fcfval  24062  tsmsxplem1  24182  tsmsxplem2  24183  tusval  24295  xpsdsfn  24408  xpsxmet  24411  xpsdsval  24412  xpsmet  24413  tmsval  24514  met1stc  24555  metuval  24583  cnmpopc  24974  pi1val  25089  pi1addf  25099  pi1addval  25100  pi1grplem  25101  rrxnm  25444  rrxcph  25445  rrxmval  25458  mbfmulc2  25717  mbfmul  25781  itg2mulclem  25801  ibladd  25876  itgadd  25880  itgabs  25890  bddmulibl  25894  dvmulf  26000  dvcmulf  26002  dvmptmul  26019  cmvth  26049  dvlip  26052  ftc1lem4  26100  mdegmullem  26137  coe1mul3  26158  r1pval  26217  plyco  26300  dgrcolem1  26333  elqaalem3  26381  taylpfval  26424  taylthlem2  26434  taylthlem2OLD  26435  pserdvlem2  26490  advlogexp  26715  logtayl  26720  logccv  26723  dvcxp1  26800  dvcncxp1  26803  logbmpt  26849  logbfval  26851  relogbf  26852  dvatan  26996  cxp2lim  27038  cxploglim2  27040  lgamgulmlem2  27091  lgamgulm2  27097  lgamcvglem  27101  lgamf  27103  basellem7  27148  basellem8  27149  basellem9  27150  fsumdvdscom  27246  logexprlim  27287  dchrfi  27317  gausslemma2dlem2  27429  gausslemma2dlem3  27430  2lgslem1b  27454  chtppilimlem2  27536  chebbnd2  27539  chto1lb  27540  chpchtlim  27541  chpo1ub  27542  vmadivsum  27544  dchrisum0lem3  27581  mudivsum  27592  logdivsum  27595  log2sumbnd  27606  selberglem1  27607  selberg2lem  27612  selberg2  27613  selbergr  27630  negsval  28075  wlkp1  29717  wwlksnextsurj  29933  wwlksnextbij  29935  clwlkclwwlklem2a1  30024  clwlkclwwlkf1  30042  eupth2eucrct  30249  frgrncvvdeq  30341  numclwlk2lem2fv  30410  numclwwlk2lem3  30412  ofoprabco  32682  fsuppcurry1  32739  fsuppcurry2  32740  offinsupp1  32741  ressprs  32936  resspos  32939  mntoval  32955  mgcoval  32959  mndlactf1  33012  mndlactfo  33013  mndractf1  33014  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  lmodvslmhm  33033  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  archirngz  33169  archiabllem2a  33174  rlocval  33231  fracval  33271  quslmod  33351  quslmhm  33352  quslvec  33353  qustriv  33357  qustrivr  33358  unitprodclb  33382  nsgmgc  33405  nsgqusf1olem1  33406  nsgqusf1olem2  33407  nsgqusf1olem3  33408  lmhmqusker  33410  rhmquskerlem  33418  elrspunidl  33421  qsidomlem1  33445  qsidomlem2  33446  opprqusbas  33481  opprqusplusg  33482  opprqusmulr  33484  opprqus1r  33485  qsdrngilem  33487  qsdrngi  33488  rprmdvdsprod  33527  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  1arithufdlem3  33539  dfufd2lem  33542  zringfrac  33547  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  ply1gsumz  33584  r1plmhm  33595  resssra  33602  ply1degltdimlem  33635  ply1degltdim  33636  qusdimsum  33641  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  lactlmhm  33647  fldgenfldext  33678  evls1fldgencl  33680  algextdeglem4  33711  algextdeglem6  33713  algextdeglem7  33714  submateq  33755  lmatcl  33762  mdetpmtr1  33769  madjusmdetlem1  33773  madjusmdetlem3  33775  qqhvval  33929  esumfzf  34033  esumpfinvallem  34038  esumpmono  34043  esummulc1  34045  esumcvg  34050  esumgect  34054  ofcval  34063  omssubadd  34265  sitgfval  34306  sitmcl  34316  sseqfv2  34359  cndprobval  34398  ballotlemfval  34454  ballotlemsv  34474  ballotlemsf1o  34478  ofcccat  34520  signsplypnf  34527  signsply0  34528  signstfval  34541  signshf  34565  reprpmtf1o  34603  reprdifc  34604  logdivsqrle  34627  hgt750lemg  34631  hgt750lema  34634  lpadval  34653  cvmliftlem8  35260  cvmliftphtlem  35285  fmla1  35355  gonarlem  35362  sategoelfvb  35387  mrsubval  35477  ellcsrspsn  35609  r1peuqusdeg1  35611  fwddifval  36126  knoppcnlem1  36459  knoppcnlem6  36464  unbdqndv2lem2  36476  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem19  37599  poimirlem22  37602  poimirlem23  37603  broucube  37614  dvtan  37630  itg2addnc  37634  ibladdnc  37637  itgaddnc  37640  itgmulc2nclem2  37647  itgmulc2nc  37648  itgabsnc  37649  ftc1cnnclem  37651  ftc1anclem3  37655  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  dvasin  37664  dvacos  37665  dvreasin  37666  dvreacos  37667  areacirclem1  37668  areacirc  37673  fsumshftd  38908  hlrelat5N  39358  rhmzrhval  41926  aks6d1c1  42073  hashscontpow  42079  aks6d1c4  42081  aks6d1c2lem3  42083  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5lem0  42092  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks6d1c5  42096  sticksstones3  42105  sticksstones8  42110  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem1  42127  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6isolem3  42133  aks6d1c6lem5  42134  aks6d1c7lem2  42138  unitscyglem1  42152  frlmfzolen  42458  frlmfzoccat  42460  frlmvscadiccat  42461  evlscl  42513  evlsval3  42514  evlsvval  42515  evlsvvval  42518  evlsbagval  42521  evlsexpval  42522  evlsaddval  42523  evlsmulval  42524  evlsevl  42526  evlcl  42527  evladdval  42530  evlmulval  42531  selvcl  42538  evlselv  42542  fsuppind  42545  mhpind  42549  mhphflem  42551  prjspner  42574  prjspnvs  42575  prjspnfv01  42579  prjspner01  42580  prjspner1  42581  0prjspnrel  42582  prjcrv0  42588  mzpclall  42683  mzpsubst  42704  eldioph2  42718  rabdiophlem2  42758  irrapxlem1  42778  mzpcong  42929  mendlmod  43150  naddcnff  43324  relexpmulnn  43671  iunrelexpuztr  43681  mnringvald  44177  mnringmulrvald  44196  radcnvrat  44283  hashnzfzclim  44291  lhe4.4ex1a  44298  expgrowthi  44302  expgrowth  44304  bccval  44307  binomcxplemrat  44319  binomcxplemfrat  44320  binomcxplemradcnv  44321  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  unirnmap  45115  unirnmapsn  45121  ssmapsn  45123  iocopn  45438  icoopn  45443  divcnvg  45548  sumnnodd  45551  climsubmpt  45581  dvsinax  45834  fperdvper  45840  dvdivf  45843  dvnprodlem1  45867  itgsincmulx  45895  stoweidlem59  45980  etransclem4  46159  etransclem13  46168  etransclem25  46180  etransclem48  46203  rrxtopnfi  46208  sge0tsms  46301  elhoi  46463  ovnval2  46466  ovnval2b  46473  ovncvrrp  46485  ovn0lem  46486  ovncl  46488  ovnome  46494  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvle  46521  ovnlecvr2  46531  ovncvr2  46532  ovnsubadd2lem  46566  ovnovollem1  46577  vonvolmbl  46582  iunhoiioolem  46596  vonioolem1  46601  vonioolem2  46602  vonicclem2  46605  smfresal  46709  smfres  46711  smfmullem4  46715  smfco  46723  adddmmbl  46754  muldmmbl  46756  fmtno  47403  isubgruhgr  47738  grtriprop  47792  grtriclwlk3  47796  intopval  47925  clintopval  47927  rngchomALTV  47991  funcringcsetcALTV2lem5  48017  ringchomALTV  48025  funcringcsetclem5ALTV  48040  srhmsubcALTVlem2  48047  srhmsubcALTV  48048  fldhmsubcALTV  48056  zlmodzxzscm  48082  zlmodzxzadd  48083  rmsupp0  48093  domnmsuppn0  48094  rmsuppss  48095  mndpsuppss  48096  ply1mulgsumlem3  48117  ply1mulgsumlem4  48118  ply1mulgsum  48119  dmatALTval  48129  lincop  48137  lincval  48138  linc1  48154  lincresunit3lem1  48208  fdivmpt  48274  fdivmptfv  48279  refdivmptfv  48280  digval  48332  2arymptfv  48384  2arymaptfo  48388  itcovalpclem1  48404  itcovalt2lem1  48409  ackvalsuc1mpt  48412  ackval1  48415  ackval2  48416  ackval3  48417  ackval42  48430  line2xlem  48487