Theorem ovexd 7170

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441  (class class class)co 7135

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-uni 4801  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  caofass  7423  caofdi  7425  caofdir  7426  caonncan  7427  suppofssd  7850  mapsnend  8571  snmapen  8573  pw2eng  8606  mapen  8665  mapxpen  8667  mapdom2  8672  cantnfcl  9114  cantnfle  9118  cantnflt  9119  cantnflt2  9120  cantnfp1lem2  9126  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1d  9135  cantnflem1  9136  cnfcomlem  9146  cnfcom  9147  cnfcom2lem  9148  cnfcom3lem  9150  fzen  12919  seqf1o  13407  wrdexg  13867  wrdnval  13888  pfxval  14026  pfxswrd  14059  splval  14104  cshwsexa  14177  ofccat  14320  climshftlem  14923  climshft  14925  climshft2  14931  caucvgr  15024  fsumrev  15126  hashdvds  16102  setsabs  16518  ressress  16554  firest  16698  prdsvscafval  16745  qusval  16807  xpsbas  16837  xpsadd  16839  xpsmul  16840  xpssca  16841  xpsvsca  16842  xpsless  16843  xpsle  16844  homfval  16954  comfval  16962  cicfval  17059  rescabs  17095  rescabs2  17096  resscat  17114  funcres2c  17163  ressffth  17200  fucbas  17222  fuccoval  17225  setchom  17332  catchom  17351  catcco  17353  estrchom  17369  funcestrcsetclem5  17386  funcsetcestrclem5  17401  evlf2val  17461  curf11  17468  curf12  17469  curf2val  17472  uncfval  17476  diagval  17482  hof2  17499  yonval  17503  gsumval2a  17887  gsumval2  17888  gsumwspan  18003  efmnd  18027  orbstafun  18433  orbstaval  18434  symgval  18489  psgnvalii  18629  lsmhash  18823  frgpupval  18892  qusabl  18978  gsumval3  19020  gsumreidx  19030  gsumzaddlem  19034  gsummptshft  19049  telgsumfzslem  19101  telgsumfz  19103  telgsumfz0  19105  dpjval  19171  srgbinomlem3  19285  srgbinomlem4  19286  mulgass3  19383  lcomfsupp  19667  rmodislmodlem  19694  rmodislmod  19695  sraval  19941  srasca  19946  crngridl  20004  quscrng  20006  znval  20227  znzrhfo  20239  znunithash  20256  cygznlem2  20260  pjfval  20395  pjpm  20397  frlmgsum  20461  frlmipval  20468  frlmphllem  20469  frlmphl  20470  frlmsslsp  20485  frlmup1  20487  gsumbagdiaglem  20613  psrass1lem  20615  psrass1  20643  psrdi  20644  psrdir  20645  psrass23l  20646  mplval  20666  mplsubglem  20672  mplsubrglem  20677  mplmonmul  20704  mplcoe1  20705  opsrval  20714  psrbagev1  20749  evlslem6  20753  evlslem1  20754  evlsval  20758  mpfconst  20773  mpff  20776  mpfaddcl  20777  mpfmulcl  20778  mpfind  20779  mhpaddcl  20799  mhpvscacl  20802  ply1lss  20825  gsumply1subr  20863  coe1add  20893  coe1tm  20902  coe1tmmul  20906  cply1mul  20923  ply1coe  20925  evl1expd  20969  pf1mpf  20976  pf1ind  20979  mamufv  20994  mamuass  21007  mamuvs1  21010  mamuvs2  21011  matgsum  21042  dmatmul  21102  scmatval  21109  scmatrhmval  21132  mvmulfv  21149  mavmulfv  21151  mavmulass  21154  marrepeval  21168  marepveval  21173  submaeval  21187  mdetrsca  21208  mdetunilem9  21225  mdetuni0  21226  gsummatr01lem3  21262  gsummatr01lem4  21263  gsummatr01  21264  smadiadetlem3  21273  cramerlem1  21292  mat2pmatmul  21336  m2cpminvid  21358  decpmatfsupp  21374  decpmatmullem  21376  decpmatmul  21377  decpmatmulsumfsupp  21378  pmatcollpw1lem1  21379  pmatcollpw3fi1lem1  21391  pmatcollpwscmatlem2  21395  pm2mpfval  21401  pm2mpf  21403  mply1topmatcllem  21408  mp2pm2mplem3  21413  mp2pm2mplem4  21414  pm2mpmhmlem1  21423  pm2mpmhmlem2  21424  pm2mp  21430  chfacfscmulfsupp  21464  chfacfscmulgsum  21465  chfacfpmmulfsupp  21468  chfacfpmmulgsum  21469  cpmidpmatlem3  21477  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  cayhamlem4  21493  xpstopnlem2  22416  fcfval  22638  tsmsxplem1  22758  tsmsxplem2  22759  tusval  22872  xpsdsfn  22984  xpsxmet  22987  xpsdsval  22988  xpsmet  22989  tmsval  23088  met1stc  23128  metuval  23156  cnmpopc  23533  pi1val  23642  pi1addf  23652  pi1addval  23653  pi1grplem  23654  rrxnm  23995  rrxcph  23996  rrxmval  24009  mbfmulc2  24267  mbfmul  24330  itg2mulclem  24350  ibladd  24424  itgadd  24428  itgabs  24438  bddmulibl  24442  dvmulf  24546  dvcmulf  24548  dvmptmul  24564  dvlip  24596  ftc1lem4  24642  mdegmullem  24679  coe1mul3  24700  r1pval  24757  plyco  24838  dgrcolem1  24870  elqaalem3  24917  taylpfval  24960  taylthlem2  24969  pserdvlem2  25023  advlogexp  25246  logtayl  25251  logccv  25254  dvcxp1  25329  dvcncxp1  25332  logbmpt  25374  logbfval  25376  relogbf  25377  dvatan  25521  cxp2lim  25562  cxploglim2  25564  lgamgulmlem2  25615  lgamgulm2  25621  lgamcvglem  25625  lgamf  25627  basellem7  25672  basellem8  25673  basellem9  25674  fsumdvdscom  25770  logexprlim  25809  dchrfi  25839  gausslemma2dlem2  25951  gausslemma2dlem3  25952  2lgslem1b  25976  chtppilimlem2  26058  chebbnd2  26061  chto1lb  26062  chpchtlim  26063  chpo1ub  26064  vmadivsum  26066  dchrisum0lem3  26103  mudivsum  26114  logdivsum  26117  log2sumbnd  26128  selberglem1  26129  selberg2lem  26134  selberg2  26135  selbergr  26152  wlkp1  27471  wwlksnextsurj  27686  wwlksnextbij  27688  clwlkclwwlklem2a1  27777  clwlkclwwlkf1  27795  eupth2eucrct  28002  frgrncvvdeq  28094  numclwlk2lem2fv  28163  numclwwlk2lem3  28165  ofoprabco  30427  fsuppcurry1  30487  fsuppcurry2  30488  offinsupp1  30489  ressprs  30668  resspos  30672  mntoval  30690  mgcoval  30694  lmodvslmhm  30735  cycpmco2f1  30816  cycpmco2rn  30817  cycpmco2lem2  30819  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2  30825  archirngz  30868  archiabllem2a  30873  frobrhm  30910  quslmod  30974  quslmhm  30975  qustriv  30980  qustrivr  30981  elrspunidl  31014  qsidomlem1  31036  qsidomlem2  31037  qusdimsum  31112  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  submateq  31162  lmatcl  31169  mdetpmtr1  31176  madjusmdetlem1  31180  madjusmdetlem3  31182  qqhvval  31334  esumfzf  31438  esumpfinvallem  31443  esumpmono  31448  esummulc1  31450  esumcvg  31455  esumgect  31459  ofcval  31468  omssubadd  31668  sitgfval  31709  sitmcl  31719  sseqfv2  31762  cndprobval  31801  ballotlemfval  31857  ballotlemsv  31877  ballotlemsf1o  31881  ofcccat  31923  signsplypnf  31930  signsply0  31931  signstfval  31944  signshf  31968  reprpmtf1o  32007  reprdifc  32008  logdivsqrle  32031  hgt750lemg  32035  hgt750lema  32038  lpadval  32057  cvmliftlem8  32652  cvmliftphtlem  32677  fmla1  32747  gonarlem  32754  sategoelfvb  32779  mrsubval  32869  fwddifval  33736  knoppcnlem1  33945  knoppcnlem6  33950  unbdqndv2lem2  33962  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem19  35076  poimirlem22  35079  poimirlem23  35080  broucube  35091  dvtan  35107  itg2addnc  35111  ibladdnc  35114  itgaddnc  35117  itgmulc2nclem2  35124  itgmulc2nc  35125  itgabsnc  35126  ftc1cnnclem  35128  ftc1anclem3  35132  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  dvasin  35141  dvacos  35142  dvreasin  35143  dvreacos  35144  areacirclem1  35145  areacirc  35150  fsumshftd  36248  hlrelat5N  36697  selvcl  39433  frlmfzolen  39437  frlmfzoccat  39439  frlmvscadiccat  39440  fsuppind  39456  prjspnval2  39611  0prjspnrel  39613  mzpclall  39668  mzpsubst  39689  eldioph2  39703  rabdiophlem2  39743  irrapxlem1  39763  mzpcong  39913  mendlmod  40137  relexpmulnn  40410  iunrelexpuztr  40420  mnringvald  40921  mnringmulrvald  40935  radcnvrat  41018  hashnzfzclim  41026  lhe4.4ex1a  41033  expgrowthi  41037  expgrowth  41039  bccval  41042  binomcxplemrat  41054  binomcxplemfrat  41055  binomcxplemradcnv  41056  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  unirnmap  41837  unirnmapsn  41843  ssmapsn  41845  iocopn  42157  icoopn  42162  divcnvg  42269  sumnnodd  42272  climsubmpt  42302  dvsinax  42555  fperdvper  42561  dvdivf  42564  dvnprodlem1  42588  itgsincmulx  42616  stoweidlem59  42701  etransclem4  42880  etransclem13  42889  etransclem25  42901  etransclem48  42924  rrxtopnfi  42929  sge0tsms  43019  elhoi  43181  ovnval2  43184  ovnval2b  43191  ovncvrrp  43203  ovn0lem  43204  ovncl  43206  ovnome  43212  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvle  43239  ovnlecvr2  43249  ovncvr2  43250  ovnsubadd2lem  43284  ovnovollem1  43295  vonvolmbl  43300  iunhoiioolem  43314  vonioolem1  43319  vonioolem2  43320  vonicclem2  43323  smfresal  43420  smfres  43422  smfmullem4  43426  smfco  43434  fmtno  44046  intopval  44462  clintopval  44464  rngcval  44586  rnghmsscmap2  44597  rnghmsscmap  44598  rngchomALTV  44609  funcrngcsetc  44622  ringcval  44632  rhmsscmap2  44643  rhmsscmap  44644  funcringcsetc  44659  funcringcsetcALTV2lem5  44664  ringchomALTV  44672  funcringcsetclem5ALTV  44687  srhmsubclem3  44699  srhmsubc  44700  fldhmsubc  44708  srhmsubcALTVlem2  44717  srhmsubcALTV  44718  fldhmsubcALTV  44726  zlmodzxzscm  44759  zlmodzxzadd  44760  rmsupp0  44770  domnmsuppn0  44771  rmsuppss  44772  ply1mulgsumlem3  44796  ply1mulgsumlem4  44797  ply1mulgsum  44798  dmatALTval  44809  lincop  44817  lincval  44818  linc1  44834  lincresunit3lem1  44888  fdivmpt  44954  fdivmptfv  44959  refdivmptfv  44960  digval  45012  2arymptfv  45064  2arymaptfo  45068  itcovalpclem1  45084  itcovalt2lem1  45089  ackvalsuc1mpt  45092  ackval1  45095  ackval2  45096  ackval3  45097  ackval42  45110  line2xlem  45167