Theorem ovexd 7290

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  caofass  7548  caofdi  7550  caofdir  7551  caonncan  7552  suppofssd  7990  mapsnend  8780  snmapen  8782  pw2eng  8818  mapen  8877  mapxpen  8879  mapunen  8882  mapdom2  8884  cantnfcl  9355  cantnfle  9359  cantnflt  9360  cantnflt2  9361  cantnfp1lem2  9367  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1d  9376  cantnflem1  9377  cnfcomlem  9387  cnfcom  9388  cnfcom2lem  9389  cnfcom3lem  9391  fzen  13202  seqf1o  13692  wrdexg  14155  wrdnval  14176  pfxval  14314  pfxswrd  14347  splval  14392  cshwsexa  14465  ofccat  14608  climshftlem  15211  climshft  15213  climshft2  15219  caucvgr  15315  fsumrev  15419  hashdvds  16404  setsabs  16808  ressress  16884  firest  17060  prdsvscafval  17108  qusval  17170  xpsbas  17200  xpsadd  17202  xpsmul  17203  xpssca  17204  xpsvsca  17205  xpsless  17206  xpsle  17207  homfval  17318  comfval  17326  cicfval  17426  rescabs  17464  rescabs2  17465  resscat  17483  funcres2c  17533  ressffth  17570  fucbas  17593  fuccoval  17597  setchom  17711  catchom  17734  catcco  17736  estrchom  17759  funcestrcsetclem5  17777  funcsetcestrclem5  17792  evlf2val  17853  curf11  17860  curf12  17861  curf2val  17864  uncfval  17868  diagval  17874  hof2  17891  yonval  17895  gsumval2a  18284  gsumval2  18285  gsumwspan  18400  efmnd  18424  orbstafun  18832  orbstaval  18833  symgval  18891  psgnvalii  19032  lsmhash  19226  frgpupval  19295  qusabl  19381  gsumval3  19423  gsumreidx  19433  gsumzaddlem  19437  gsummptshft  19452  telgsumfzslem  19504  telgsumfz  19506  telgsumfz0  19508  dpjval  19574  srgbinomlem3  19693  srgbinomlem4  19694  mulgass3  19794  lcomfsupp  20078  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  sraval  20353  srasca  20362  crngridl  20422  quscrng  20424  znval  20651  znzrhfo  20667  znunithash  20684  cygznlem2  20688  pjfval  20823  pjpm  20825  frlmgsum  20889  frlmipval  20896  frlmphllem  20897  frlmphl  20898  frlmsslsp  20913  frlmup1  20915  gsumbagdiaglemOLD  21051  psrass1lemOLD  21053  gsumbagdiaglem  21054  psrass1lem  21056  psrass1  21084  psrdi  21085  psrdir  21086  psrass23l  21087  mplval  21107  mplsubglem  21115  mplsubrglem  21120  mplmonmul  21147  mplcoe1  21148  opsrval  21157  psrbagev1  21195  psrbagev1OLD  21196  psrbagev2  21197  evlslem6  21201  evlslem1  21202  evlsval  21206  mpfconst  21221  mpff  21224  mpfaddcl  21225  mpfmulcl  21226  mpfind  21227  mhpmulcl  21249  mhpaddcl  21251  mhpvscacl  21254  ply1lss  21277  gsumply1subr  21315  coe1add  21345  coe1tm  21354  coe1tmmul  21358  cply1mul  21375  ply1coe  21377  evl1expd  21421  pf1mpf  21428  pf1ind  21431  mamufv  21446  mamuass  21459  mamuvs1  21462  mamuvs2  21463  matgsum  21494  dmatmul  21554  scmatval  21561  scmatrhmval  21584  mvmulfv  21601  mavmulfv  21603  mavmulass  21606  marrepeval  21620  marepveval  21625  submaeval  21639  mdetrsca  21660  mdetunilem9  21677  mdetuni0  21678  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  smadiadetlem3  21725  cramerlem1  21744  mat2pmatmul  21788  m2cpminvid  21810  decpmatfsupp  21826  decpmatmullem  21828  decpmatmul  21829  decpmatmulsumfsupp  21830  pmatcollpw1lem1  21831  pmatcollpw3fi1lem1  21843  pmatcollpwscmatlem2  21847  pm2mpfval  21853  pm2mpf  21855  mply1topmatcllem  21860  mp2pm2mplem3  21865  mp2pm2mplem4  21866  pm2mpmhmlem1  21875  pm2mpmhmlem2  21876  pm2mp  21882  chfacfscmulfsupp  21916  chfacfscmulgsum  21917  chfacfpmmulfsupp  21920  chfacfpmmulgsum  21921  cpmidpmatlem3  21929  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cayhamlem4  21945  xpstopnlem2  22870  fcfval  23092  tsmsxplem1  23212  tsmsxplem2  23213  tusval  23325  xpsdsfn  23438  xpsxmet  23441  xpsdsval  23442  xpsmet  23443  tmsval  23542  met1stc  23583  metuval  23611  cnmpopc  23997  pi1val  24106  pi1addf  24116  pi1addval  24117  pi1grplem  24118  rrxnm  24460  rrxcph  24461  rrxmval  24474  mbfmulc2  24732  mbfmul  24796  itg2mulclem  24816  ibladd  24890  itgadd  24894  itgabs  24904  bddmulibl  24908  dvmulf  25012  dvcmulf  25014  dvmptmul  25030  dvlip  25062  ftc1lem4  25108  mdegmullem  25148  coe1mul3  25169  r1pval  25226  plyco  25307  dgrcolem1  25339  elqaalem3  25386  taylpfval  25429  taylthlem2  25438  pserdvlem2  25492  advlogexp  25715  logtayl  25720  logccv  25723  dvcxp1  25798  dvcncxp1  25801  logbmpt  25843  logbfval  25845  relogbf  25846  dvatan  25990  cxp2lim  26031  cxploglim2  26033  lgamgulmlem2  26084  lgamgulm2  26090  lgamcvglem  26094  lgamf  26096  basellem7  26141  basellem8  26142  basellem9  26143  fsumdvdscom  26239  logexprlim  26278  dchrfi  26308  gausslemma2dlem2  26420  gausslemma2dlem3  26421  2lgslem1b  26445  chtppilimlem2  26527  chebbnd2  26530  chto1lb  26531  chpchtlim  26532  chpo1ub  26533  vmadivsum  26535  dchrisum0lem3  26572  mudivsum  26583  logdivsum  26586  log2sumbnd  26597  selberglem1  26598  selberg2lem  26603  selberg2  26604  selbergr  26621  wlkp1  27951  wwlksnextsurj  28166  wwlksnextbij  28168  clwlkclwwlklem2a1  28257  clwlkclwwlkf1  28275  eupth2eucrct  28482  frgrncvvdeq  28574  numclwlk2lem2fv  28643  numclwwlk2lem3  28645  ofoprabco  30903  fsuppcurry1  30962  fsuppcurry2  30963  offinsupp1  30964  ressprs  31143  resspos  31146  mntoval  31162  mgcoval  31166  lmodvslmhm  31212  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem2  31296  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2  31302  archirngz  31345  archiabllem2a  31350  frobrhm  31387  quslmod  31456  quslmhm  31457  qustriv  31462  qustrivr  31463  nsgmgc  31499  nsgqusf1olem1  31500  nsgqusf1olem2  31501  nsgqusf1olem3  31502  elrspunidl  31508  qsidomlem1  31530  qsidomlem2  31531  qusdimsum  31611  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  submateq  31661  lmatcl  31668  mdetpmtr1  31675  madjusmdetlem1  31679  madjusmdetlem3  31681  qqhvval  31833  esumfzf  31937  esumpfinvallem  31942  esumpmono  31947  esummulc1  31949  esumcvg  31954  esumgect  31958  ofcval  31967  omssubadd  32167  sitgfval  32208  sitmcl  32218  sseqfv2  32261  cndprobval  32300  ballotlemfval  32356  ballotlemsv  32376  ballotlemsf1o  32380  ofcccat  32422  signsplypnf  32429  signsply0  32430  signstfval  32443  signshf  32467  reprpmtf1o  32506  reprdifc  32507  logdivsqrle  32530  hgt750lemg  32534  hgt750lema  32537  lpadval  32556  cvmliftlem8  33154  cvmliftphtlem  33179  fmla1  33249  gonarlem  33256  sategoelfvb  33281  mrsubval  33371  negsval  34050  fwddifval  34391  knoppcnlem1  34600  knoppcnlem6  34605  unbdqndv2lem2  34617  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem19  35723  poimirlem22  35726  poimirlem23  35727  broucube  35738  dvtan  35754  itg2addnc  35758  ibladdnc  35761  itgaddnc  35764  itgmulc2nclem2  35771  itgmulc2nc  35772  itgabsnc  35773  ftc1cnnclem  35775  ftc1anclem3  35779  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  dvasin  35788  dvacos  35789  dvreasin  35790  dvreacos  35791  areacirclem1  35792  areacirc  35797  fsumshftd  36893  hlrelat5N  37342  sticksstones3  40032  sticksstones8  40037  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  selvcl  40156  frlmfzolen  40160  frlmfzoccat  40162  frlmvscadiccat  40163  evlsval3  40195  evlsbagval  40198  evlsexpval  40199  evlsaddval  40200  evlsmulval  40201  fsuppind  40202  mhpind  40206  mhphflem  40207  prjspner  40379  prjspnvs  40380  prjspnfv01  40382  prjspner01  40383  prjspner1  40384  0prjspnrel  40385  mzpclall  40465  mzpsubst  40486  eldioph2  40500  rabdiophlem2  40540  irrapxlem1  40560  mzpcong  40710  mendlmod  40934  relexpmulnn  41206  iunrelexpuztr  41216  mnringvald  41715  mnringmulrvald  41734  radcnvrat  41821  hashnzfzclim  41829  lhe4.4ex1a  41836  expgrowthi  41840  expgrowth  41842  bccval  41845  binomcxplemrat  41857  binomcxplemfrat  41858  binomcxplemradcnv  41859  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  unirnmap  42637  unirnmapsn  42643  ssmapsn  42645  iocopn  42948  icoopn  42953  divcnvg  43058  sumnnodd  43061  climsubmpt  43091  dvsinax  43344  fperdvper  43350  dvdivf  43353  dvnprodlem1  43377  itgsincmulx  43405  stoweidlem59  43490  etransclem4  43669  etransclem13  43678  etransclem25  43690  etransclem48  43713  rrxtopnfi  43718  sge0tsms  43808  elhoi  43970  ovnval2  43973  ovnval2b  43980  ovncvrrp  43992  ovn0lem  43993  ovncl  43995  ovnome  44001  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvle  44028  ovnlecvr2  44038  ovncvr2  44039  ovnsubadd2lem  44073  ovnovollem1  44084  vonvolmbl  44089  iunhoiioolem  44103  vonioolem1  44108  vonioolem2  44109  vonicclem2  44112  smfresal  44209  smfres  44211  smfmullem4  44215  smfco  44223  fmtno  44869  intopval  45284  clintopval  45286  rngcval  45408  rnghmsscmap2  45419  rnghmsscmap  45420  rngchomALTV  45431  funcrngcsetc  45444  ringcval  45454  rhmsscmap2  45465  rhmsscmap  45466  funcringcsetc  45481  funcringcsetcALTV2lem5  45486  ringchomALTV  45494  funcringcsetclem5ALTV  45509  srhmsubclem3  45521  srhmsubc  45522  fldhmsubc  45530  srhmsubcALTVlem2  45539  srhmsubcALTV  45540  fldhmsubcALTV  45548  zlmodzxzscm  45581  zlmodzxzadd  45582  rmsupp0  45592  domnmsuppn0  45593  rmsuppss  45594  mndpsuppss  45595  ply1mulgsumlem3  45617  ply1mulgsumlem4  45618  ply1mulgsum  45619  dmatALTval  45629  lincop  45637  lincval  45638  linc1  45654  lincresunit3lem1  45708  fdivmpt  45774  fdivmptfv  45779  refdivmptfv  45780  digval  45832  2arymptfv  45884  2arymaptfo  45888  itcovalpclem1  45904  itcovalt2lem1  45909  ackvalsuc1mpt  45912  ackval1  45915  ackval2  45916  ackval3  45917  ackval42  45930  line2xlem  45987