Theorem ovexd 7441

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  (class class class)co 7406

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-ext 2704  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-pr 4631  df-uni 4909  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  caofass  7704  caofdi  7706  caofdir  7707  caonncan  7708  suppofssd  8185  mapsnend  9033  snmapen  9035  pw2eng  9075  mapen  9138  mapxpen  9140  mapunen  9143  mapdom2  9145  cantnfcl  9659  cantnfle  9663  cantnflt  9664  cantnflt2  9665  cantnfp1lem2  9671  cantnfp1lem3  9672  cantnflem1b  9678  cantnflem1d  9680  cantnflem1  9681  cnfcomlem  9691  cnfcom  9692  cnfcom2lem  9693  cnfcom3lem  9695  fzen  13515  seqf1o  14006  wrdexg  14471  wrdnval  14492  pfxval  14620  pfxswrd  14653  splval  14698  cshwsexaOLD  14772  ofccat  14913  climshftlem  15515  climshft  15517  climshft2  15523  caucvgr  15619  fsumrev  15722  hashdvds  16705  setsabs  17109  ressress  17190  firest  17375  prdsvscafval  17423  qusval  17485  xpsbas  17515  xpsadd  17517  xpsmul  17518  xpssca  17519  xpsvsca  17520  xpsless  17521  xpsle  17522  homfval  17633  comfval  17641  cicfval  17741  rescabs  17779  rescabsOLD  17780  rescabs2  17781  resscat  17799  funcres2c  17849  ressffth  17886  fucbas  17909  fuccoval  17913  setchom  18027  catchom  18050  catcco  18052  estrchom  18075  funcestrcsetclem5  18093  funcsetcestrclem5  18108  evlf2val  18169  curf11  18176  curf12  18177  curf2val  18180  uncfval  18184  diagval  18190  hof2  18207  yonval  18211  gsumval2a  18601  gsumval2  18602  gsumwspan  18724  efmnd  18748  orbstafun  19170  orbstaval  19171  symgval  19231  psgnvalii  19372  lsmhash  19568  frgpupval  19637  qusabl  19728  gsumval3  19770  gsumreidx  19780  gsumzaddlem  19784  gsummptshft  19799  telgsumfzslem  19851  telgsumfz  19853  telgsumfz0  19855  dpjval  19921  srgbinomlem3  20045  srgbinomlem4  20046  mulgass3  20160  lcomfsupp  20505  rmodislmodlem  20532  rmodislmod  20533  rmodislmodOLD  20534  sraval  20782  srasca  20791  srascaOLD  20792  crngridl  20869  quscrng  20871  znval  21079  znzrhfo  21095  znunithash  21112  cygznlem2  21116  pjfval  21253  pjpm  21255  frlmgsum  21319  frlmipval  21326  frlmphllem  21327  frlmphl  21328  frlmsslsp  21343  frlmup1  21345  gsumbagdiaglemOLD  21483  psrass1lemOLD  21485  gsumbagdiaglem  21486  psrass1lem  21488  psrass1  21517  psrdi  21518  psrdir  21519  psrass23l  21520  mplval  21540  mplsubglem  21550  mplsubrglem  21555  mplmonmul  21583  mplcoe1  21584  opsrval  21593  psrbagev1  21630  psrbagev1OLD  21631  psrbagev2  21632  evlslem6  21636  evlslem1  21637  evlsval  21641  mpfconst  21656  mpff  21659  mpfaddcl  21660  mpfmulcl  21661  mpfind  21662  mhpmulcl  21684  mhpaddcl  21686  mhpvscacl  21689  ply1lss  21712  gsumply1subr  21748  coe1add  21778  coe1tm  21787  coe1tmmul  21791  cply1mul  21810  ply1coe  21812  evl1expd  21856  pf1mpf  21863  pf1ind  21866  mamufv  21881  mamuass  21894  mamuvs1  21897  mamuvs2  21898  matgsum  21931  dmatmul  21991  scmatval  21998  scmatrhmval  22021  mvmulfv  22038  mavmulfv  22040  mavmulass  22043  marrepeval  22057  marepveval  22062  submaeval  22076  mdetrsca  22097  mdetunilem9  22114  mdetuni0  22115  gsummatr01lem3  22151  gsummatr01lem4  22152  gsummatr01  22153  smadiadetlem3  22162  cramerlem1  22181  mat2pmatmul  22225  m2cpminvid  22247  decpmatfsupp  22263  decpmatmullem  22265  decpmatmul  22266  decpmatmulsumfsupp  22267  pmatcollpw1lem1  22268  pmatcollpw3fi1lem1  22280  pmatcollpwscmatlem2  22284  pm2mpfval  22290  pm2mpf  22292  mply1topmatcllem  22297  mp2pm2mplem3  22302  mp2pm2mplem4  22303  pm2mpmhmlem1  22312  pm2mpmhmlem2  22313  pm2mp  22319  chfacfscmulfsupp  22353  chfacfscmulgsum  22354  chfacfpmmulfsupp  22357  chfacfpmmulgsum  22358  cpmidpmatlem3  22366  cpmadugsumlemB  22368  cpmadugsumlemC  22369  cpmadugsumlemF  22370  cayhamlem4  22382  xpstopnlem2  23307  fcfval  23529  tsmsxplem1  23649  tsmsxplem2  23650  tusval  23762  xpsdsfn  23875  xpsxmet  23878  xpsdsval  23879  xpsmet  23880  tmsval  23981  met1stc  24022  metuval  24050  cnmpopc  24436  pi1val  24545  pi1addf  24555  pi1addval  24556  pi1grplem  24557  rrxnm  24900  rrxcph  24901  rrxmval  24914  mbfmulc2  25172  mbfmul  25236  itg2mulclem  25256  ibladd  25330  itgadd  25334  itgabs  25344  bddmulibl  25348  dvmulf  25452  dvcmulf  25454  dvmptmul  25470  dvlip  25502  ftc1lem4  25548  mdegmullem  25588  coe1mul3  25609  r1pval  25666  plyco  25747  dgrcolem1  25779  elqaalem3  25826  taylpfval  25869  taylthlem2  25878  pserdvlem2  25932  advlogexp  26155  logtayl  26160  logccv  26163  dvcxp1  26238  dvcncxp1  26241  logbmpt  26283  logbfval  26285  relogbf  26286  dvatan  26430  cxp2lim  26471  cxploglim2  26473  lgamgulmlem2  26524  lgamgulm2  26530  lgamcvglem  26534  lgamf  26536  basellem7  26581  basellem8  26582  basellem9  26583  fsumdvdscom  26679  logexprlim  26718  dchrfi  26748  gausslemma2dlem2  26860  gausslemma2dlem3  26861  2lgslem1b  26885  chtppilimlem2  26967  chebbnd2  26970  chto1lb  26971  chpchtlim  26972  chpo1ub  26973  vmadivsum  26975  dchrisum0lem3  27012  mudivsum  27023  logdivsum  27026  log2sumbnd  27037  selberglem1  27038  selberg2lem  27043  selberg2  27044  selbergr  27061  negsval  27490  wlkp1  28928  wwlksnextsurj  29144  wwlksnextbij  29146  clwlkclwwlklem2a1  29235  clwlkclwwlkf1  29253  eupth2eucrct  29460  frgrncvvdeq  29552  numclwlk2lem2fv  29621  numclwwlk2lem3  29623  ofoprabco  31877  fsuppcurry1  31938  fsuppcurry2  31939  offinsupp1  31940  ressprs  32121  resspos  32124  mntoval  32140  mgcoval  32144  lmodvslmhm  32190  cycpmco2f1  32271  cycpmco2rn  32272  cycpmco2lem2  32274  cycpmco2lem3  32275  cycpmco2lem4  32276  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2  32280  archirngz  32323  archiabllem2a  32328  frobrhm  32371  quslmod  32458  quslmhm  32459  quslvec  32460  qustriv  32465  qustrivr  32466  nsgmgc  32512  nsgqusf1olem1  32513  nsgqusf1olem2  32514  nsgqusf1olem3  32515  ghmquskerlem1  32517  ghmquskerco  32518  ghmquskerlem2  32519  ghmquskerlem3  32520  ghmqusker  32521  lmhmqusker  32523  rhmquskerlem  32532  elrspunidl  32535  qsidomlem1  32560  qsidomlem2  32561  opprqusbas  32591  opprqusplusg  32592  opprqusmulr  32594  opprqus1r  32595  qsdrngilem  32597  qsdrngi  32598  ply1gsumz  32658  ply1degltdimlem  32696  ply1degltdim  32697  qusdimsum  32702  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  algextdeglem1  32761  submateq  32778  lmatcl  32785  mdetpmtr1  32792  madjusmdetlem1  32796  madjusmdetlem3  32798  qqhvval  32952  esumfzf  33056  esumpfinvallem  33061  esumpmono  33066  esummulc1  33068  esumcvg  33073  esumgect  33077  ofcval  33086  omssubadd  33288  sitgfval  33329  sitmcl  33339  sseqfv2  33382  cndprobval  33421  ballotlemfval  33477  ballotlemsv  33497  ballotlemsf1o  33501  ofcccat  33543  signsplypnf  33550  signsply0  33551  signstfval  33564  signshf  33588  reprpmtf1o  33627  reprdifc  33628  logdivsqrle  33651  hgt750lemg  33655  hgt750lema  33658  lpadval  33677  cvmliftlem8  34272  cvmliftphtlem  34297  fmla1  34367  gonarlem  34374  sategoelfvb  34399  mrsubval  34489  fwddifval  35123  gg-cmvth  35170  knoppcnlem1  35358  knoppcnlem6  35363  unbdqndv2lem2  35375  poimirlem1  36478  poimirlem2  36479  poimirlem3  36480  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem19  36496  poimirlem22  36499  poimirlem23  36500  broucube  36511  dvtan  36527  itg2addnc  36531  ibladdnc  36534  itgaddnc  36537  itgmulc2nclem2  36544  itgmulc2nc  36545  itgabsnc  36546  ftc1cnnclem  36548  ftc1anclem3  36552  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  dvasin  36561  dvacos  36562  dvreasin  36563  dvreacos  36564  areacirclem1  36565  areacirc  36570  fsumshftd  37811  hlrelat5N  38261  sticksstones3  40953  sticksstones8  40958  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  frlmfzolen  41075  frlmfzoccat  41077  frlmvscadiccat  41078  rhmmpllem1  41119  rhmmpl  41123  evlscl  41128  evlsval3  41129  evlsvval  41130  evlsvvval  41133  evlsbagval  41136  evlsexpval  41137  evlsaddval  41138  evlsmulval  41139  evlsevl  41141  evlcl  41142  evladdval  41145  evlmulval  41146  selvcl  41153  evlselv  41157  fsuppind  41160  mhpind  41164  mhphflem  41166  prjspner  41358  prjspnvs  41359  prjspnfv01  41363  prjspner01  41364  prjspner1  41365  0prjspnrel  41366  prjcrv0  41372  mzpclall  41451  mzpsubst  41472  eldioph2  41486  rabdiophlem2  41526  irrapxlem1  41546  mzpcong  41697  mendlmod  41921  naddcnff  42098  relexpmulnn  42446  iunrelexpuztr  42456  mnringvald  42953  mnringmulrvald  42972  radcnvrat  43059  hashnzfzclim  43067  lhe4.4ex1a  43074  expgrowthi  43078  expgrowth  43080  bccval  43083  binomcxplemrat  43095  binomcxplemfrat  43096  binomcxplemradcnv  43097  binomcxplemdvbinom  43098  binomcxplemdvsum  43100  binomcxplemnotnn0  43101  unirnmap  43893  unirnmapsn  43899  ssmapsn  43901  iocopn  44220  icoopn  44225  divcnvg  44330  sumnnodd  44333  climsubmpt  44363  dvsinax  44616  fperdvper  44622  dvdivf  44625  dvnprodlem1  44649  itgsincmulx  44677  stoweidlem59  44762  etransclem4  44941  etransclem13  44950  etransclem25  44962  etransclem48  44985  rrxtopnfi  44990  sge0tsms  45083  elhoi  45245  ovnval2  45248  ovnval2b  45255  ovncvrrp  45267  ovn0lem  45268  ovncl  45270  ovnome  45276  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvle  45303  ovnlecvr2  45313  ovncvr2  45314  ovnsubadd2lem  45348  ovnovollem1  45359  vonvolmbl  45364  iunhoiioolem  45378  vonioolem1  45383  vonioolem2  45384  vonicclem2  45387  smfresal  45491  smfres  45493  smfmullem4  45497  smfco  45505  adddmmbl  45536  muldmmbl  45538  fmtno  46184  intopval  46599  clintopval  46601  prdsrngd  46664  rngcval  46814  rnghmsscmap2  46825  rnghmsscmap  46826  rngchomALTV  46837  funcrngcsetc  46850  ringcval  46860  rhmsscmap2  46871  rhmsscmap  46872  funcringcsetc  46887  funcringcsetcALTV2lem5  46892  ringchomALTV  46900  funcringcsetclem5ALTV  46915  srhmsubclem3  46927  srhmsubc  46928  fldhmsubc  46936  srhmsubcALTVlem2  46945  srhmsubcALTV  46946  fldhmsubcALTV  46954  zlmodzxzscm  46987  zlmodzxzadd  46988  rmsupp0  46998  domnmsuppn0  46999  rmsuppss  47000  mndpsuppss  47001  ply1mulgsumlem3  47023  ply1mulgsumlem4  47024  ply1mulgsum  47025  dmatALTval  47035  lincop  47043  lincval  47044  linc1  47060  lincresunit3lem1  47114  fdivmpt  47180  fdivmptfv  47185  refdivmptfv  47186  digval  47238  2arymptfv  47290  2arymaptfo  47294  itcovalpclem1  47310  itcovalt2lem1  47315  ackvalsuc1mpt  47318  ackval1  47321  ackval2  47322  ackval3  47323  ackval42  47336  line2xlem  47393