Theorem ovexd 7319

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433  (class class class)co 7284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-sn 4563  df-pr 4565  df-uni 4841  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  caofass  7579  caofdi  7581  caofdir  7582  caonncan  7583  suppofssd  8028  mapsnend  8835  snmapen  8837  pw2eng  8874  mapen  8937  mapxpen  8939  mapunen  8942  mapdom2  8944  cantnfcl  9434  cantnfle  9438  cantnflt  9439  cantnflt2  9440  cantnfp1lem2  9446  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1d  9455  cantnflem1  9456  cnfcomlem  9466  cnfcom  9467  cnfcom2lem  9468  cnfcom3lem  9470  fzen  13282  seqf1o  13773  wrdexg  14236  wrdnval  14257  pfxval  14395  pfxswrd  14428  splval  14473  cshwsexa  14546  ofccat  14689  climshftlem  15292  climshft  15294  climshft2  15300  caucvgr  15396  fsumrev  15500  hashdvds  16485  setsabs  16889  ressress  16967  firest  17152  prdsvscafval  17200  qusval  17262  xpsbas  17292  xpsadd  17294  xpsmul  17295  xpssca  17296  xpsvsca  17297  xpsless  17298  xpsle  17299  homfval  17410  comfval  17418  cicfval  17518  rescabs  17556  rescabsOLD  17557  rescabs2  17558  resscat  17576  funcres2c  17626  ressffth  17663  fucbas  17686  fuccoval  17690  setchom  17804  catchom  17827  catcco  17829  estrchom  17852  funcestrcsetclem5  17870  funcsetcestrclem5  17885  evlf2val  17946  curf11  17953  curf12  17954  curf2val  17957  uncfval  17961  diagval  17967  hof2  17984  yonval  17988  gsumval2a  18378  gsumval2  18379  gsumwspan  18494  efmnd  18518  orbstafun  18926  orbstaval  18927  symgval  18985  psgnvalii  19126  lsmhash  19320  frgpupval  19389  qusabl  19475  gsumval3  19517  gsumreidx  19527  gsumzaddlem  19531  gsummptshft  19546  telgsumfzslem  19598  telgsumfz  19600  telgsumfz0  19602  dpjval  19668  srgbinomlem3  19787  srgbinomlem4  19788  mulgass3  19888  lcomfsupp  20172  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  sraval  20447  srasca  20456  srascaOLD  20457  crngridl  20518  quscrng  20520  znval  20748  znzrhfo  20764  znunithash  20781  cygznlem2  20785  pjfval  20922  pjpm  20924  frlmgsum  20988  frlmipval  20995  frlmphllem  20996  frlmphl  20997  frlmsslsp  21012  frlmup1  21014  gsumbagdiaglemOLD  21150  psrass1lemOLD  21152  gsumbagdiaglem  21153  psrass1lem  21155  psrass1  21183  psrdi  21184  psrdir  21185  psrass23l  21186  mplval  21206  mplsubglem  21214  mplsubrglem  21219  mplmonmul  21246  mplcoe1  21247  opsrval  21256  psrbagev1  21294  psrbagev1OLD  21295  psrbagev2  21296  evlslem6  21300  evlslem1  21301  evlsval  21305  mpfconst  21320  mpff  21323  mpfaddcl  21324  mpfmulcl  21325  mpfind  21326  mhpmulcl  21348  mhpaddcl  21350  mhpvscacl  21353  ply1lss  21376  gsumply1subr  21414  coe1add  21444  coe1tm  21453  coe1tmmul  21457  cply1mul  21474  ply1coe  21476  evl1expd  21520  pf1mpf  21527  pf1ind  21530  mamufv  21545  mamuass  21558  mamuvs1  21561  mamuvs2  21562  matgsum  21595  dmatmul  21655  scmatval  21662  scmatrhmval  21685  mvmulfv  21702  mavmulfv  21704  mavmulass  21707  marrepeval  21721  marepveval  21726  submaeval  21740  mdetrsca  21761  mdetunilem9  21778  mdetuni0  21779  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  smadiadetlem3  21826  cramerlem1  21845  mat2pmatmul  21889  m2cpminvid  21911  decpmatfsupp  21927  decpmatmullem  21929  decpmatmul  21930  decpmatmulsumfsupp  21931  pmatcollpw1lem1  21932  pmatcollpw3fi1lem1  21944  pmatcollpwscmatlem2  21948  pm2mpfval  21954  pm2mpf  21956  mply1topmatcllem  21961  mp2pm2mplem3  21966  mp2pm2mplem4  21967  pm2mpmhmlem1  21976  pm2mpmhmlem2  21977  pm2mp  21983  chfacfscmulfsupp  22017  chfacfscmulgsum  22018  chfacfpmmulfsupp  22021  chfacfpmmulgsum  22022  cpmidpmatlem3  22030  cpmadugsumlemB  22032  cpmadugsumlemC  22033  cpmadugsumlemF  22034  cayhamlem4  22046  xpstopnlem2  22971  fcfval  23193  tsmsxplem1  23313  tsmsxplem2  23314  tusval  23426  xpsdsfn  23539  xpsxmet  23542  xpsdsval  23543  xpsmet  23544  tmsval  23645  met1stc  23686  metuval  23714  cnmpopc  24100  pi1val  24209  pi1addf  24219  pi1addval  24220  pi1grplem  24221  rrxnm  24564  rrxcph  24565  rrxmval  24578  mbfmulc2  24836  mbfmul  24900  itg2mulclem  24920  ibladd  24994  itgadd  24998  itgabs  25008  bddmulibl  25012  dvmulf  25116  dvcmulf  25118  dvmptmul  25134  dvlip  25166  ftc1lem4  25212  mdegmullem  25252  coe1mul3  25273  r1pval  25330  plyco  25411  dgrcolem1  25443  elqaalem3  25490  taylpfval  25533  taylthlem2  25542  pserdvlem2  25596  advlogexp  25819  logtayl  25824  logccv  25827  dvcxp1  25902  dvcncxp1  25905  logbmpt  25947  logbfval  25949  relogbf  25950  dvatan  26094  cxp2lim  26135  cxploglim2  26137  lgamgulmlem2  26188  lgamgulm2  26194  lgamcvglem  26198  lgamf  26200  basellem7  26245  basellem8  26246  basellem9  26247  fsumdvdscom  26343  logexprlim  26382  dchrfi  26412  gausslemma2dlem2  26524  gausslemma2dlem3  26525  2lgslem1b  26549  chtppilimlem2  26631  chebbnd2  26634  chto1lb  26635  chpchtlim  26636  chpo1ub  26637  vmadivsum  26639  dchrisum0lem3  26676  mudivsum  26687  logdivsum  26690  log2sumbnd  26701  selberglem1  26702  selberg2lem  26707  selberg2  26708  selbergr  26725  wlkp1  28058  wwlksnextsurj  28274  wwlksnextbij  28276  clwlkclwwlklem2a1  28365  clwlkclwwlkf1  28383  eupth2eucrct  28590  frgrncvvdeq  28682  numclwlk2lem2fv  28751  numclwwlk2lem3  28753  ofoprabco  31010  fsuppcurry1  31069  fsuppcurry2  31070  offinsupp1  31071  ressprs  31250  resspos  31253  mntoval  31269  mgcoval  31273  lmodvslmhm  31319  cycpmco2f1  31400  cycpmco2rn  31401  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2  31409  archirngz  31452  archiabllem2a  31457  frobrhm  31494  quslmod  31563  quslmhm  31564  qustriv  31569  qustrivr  31570  nsgmgc  31606  nsgqusf1olem1  31607  nsgqusf1olem2  31608  nsgqusf1olem3  31609  elrspunidl  31615  qsidomlem1  31637  qsidomlem2  31638  qusdimsum  31718  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  submateq  31768  lmatcl  31775  mdetpmtr1  31782  madjusmdetlem1  31786  madjusmdetlem3  31788  qqhvval  31942  esumfzf  32046  esumpfinvallem  32051  esumpmono  32056  esummulc1  32058  esumcvg  32063  esumgect  32067  ofcval  32076  omssubadd  32276  sitgfval  32317  sitmcl  32327  sseqfv2  32370  cndprobval  32409  ballotlemfval  32465  ballotlemsv  32485  ballotlemsf1o  32489  ofcccat  32531  signsplypnf  32538  signsply0  32539  signstfval  32552  signshf  32576  reprpmtf1o  32615  reprdifc  32616  logdivsqrle  32639  hgt750lemg  32643  hgt750lema  32646  lpadval  32665  cvmliftlem8  33263  cvmliftphtlem  33288  fmla1  33358  gonarlem  33365  sategoelfvb  33390  mrsubval  33480  negsval  34132  fwddifval  34473  knoppcnlem1  34682  knoppcnlem6  34687  unbdqndv2lem2  34699  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem19  35805  poimirlem22  35808  poimirlem23  35809  broucube  35820  dvtan  35836  itg2addnc  35840  ibladdnc  35843  itgaddnc  35846  itgmulc2nclem2  35853  itgmulc2nc  35854  itgabsnc  35855  ftc1cnnclem  35857  ftc1anclem3  35861  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  dvasin  35870  dvacos  35871  dvreasin  35872  dvreacos  35873  areacirclem1  35874  areacirc  35879  fsumshftd  36973  hlrelat5N  37422  sticksstones3  40111  sticksstones8  40116  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  selvcl  40237  frlmfzolen  40241  frlmfzoccat  40243  frlmvscadiccat  40244  evlsval3  40279  evlsbagval  40282  evlsexpval  40283  evlsaddval  40284  evlsmulval  40285  fsuppind  40286  mhpind  40290  mhphflem  40291  prjspner  40465  prjspnvs  40466  prjspnfv01  40468  prjspner01  40469  prjspner1  40470  0prjspnrel  40471  prjcrv0  40477  mzpclall  40556  mzpsubst  40577  eldioph2  40591  rabdiophlem2  40631  irrapxlem1  40651  mzpcong  40801  mendlmod  41025  relexpmulnn  41324  iunrelexpuztr  41334  mnringvald  41833  mnringmulrvald  41852  radcnvrat  41939  hashnzfzclim  41947  lhe4.4ex1a  41954  expgrowthi  41958  expgrowth  41960  bccval  41963  binomcxplemrat  41975  binomcxplemfrat  41976  binomcxplemradcnv  41977  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  unirnmap  42755  unirnmapsn  42761  ssmapsn  42763  iocopn  43065  icoopn  43070  divcnvg  43175  sumnnodd  43178  climsubmpt  43208  dvsinax  43461  fperdvper  43467  dvdivf  43470  dvnprodlem1  43494  itgsincmulx  43522  stoweidlem59  43607  etransclem4  43786  etransclem13  43795  etransclem25  43807  etransclem48  43830  rrxtopnfi  43835  sge0tsms  43925  elhoi  44087  ovnval2  44090  ovnval2b  44097  ovncvrrp  44109  ovn0lem  44110  ovncl  44112  ovnome  44118  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvle  44145  ovnlecvr2  44155  ovncvr2  44156  ovnsubadd2lem  44190  ovnovollem1  44201  vonvolmbl  44206  iunhoiioolem  44220  vonioolem1  44225  vonioolem2  44226  vonicclem2  44229  smfresal  44333  smfres  44335  smfmullem4  44339  smfco  44347  fmtno  44992  intopval  45407  clintopval  45409  rngcval  45531  rnghmsscmap2  45542  rnghmsscmap  45543  rngchomALTV  45554  funcrngcsetc  45567  ringcval  45577  rhmsscmap2  45588  rhmsscmap  45589  funcringcsetc  45604  funcringcsetcALTV2lem5  45609  ringchomALTV  45617  funcringcsetclem5ALTV  45632  srhmsubclem3  45644  srhmsubc  45645  fldhmsubc  45653  srhmsubcALTVlem2  45662  srhmsubcALTV  45663  fldhmsubcALTV  45671  zlmodzxzscm  45704  zlmodzxzadd  45705  rmsupp0  45715  domnmsuppn0  45716  rmsuppss  45717  mndpsuppss  45718  ply1mulgsumlem3  45740  ply1mulgsumlem4  45741  ply1mulgsum  45742  dmatALTval  45752  lincop  45760  lincval  45761  linc1  45777  lincresunit3lem1  45831  fdivmpt  45897  fdivmptfv  45902  refdivmptfv  45903  digval  45955  2arymptfv  46007  2arymaptfo  46011  itcovalpclem1  46027  itcovalt2lem1  46032  ackvalsuc1mpt  46035  ackval1  46038  ackval2  46039  ackval3  46040  ackval42  46053  line2xlem  46110