Theorem ovexd 7433

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-nul 5258

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  caofidlcan  7700  caofass  7702  caofdi  7704  caofdir  7705  caonncan  7706  suppofssd  8185  mapsnend  9019  snmapen  9021  pw2eng  9057  mapen  9115  mapxpen  9117  mapunen  9120  mapdom2  9122  cantnfcl  9624  cantnfle  9628  cantnflt  9629  cantnflt2  9630  cantnfp1lem2  9636  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1d  9645  cantnflem1  9646  cnfcomlem  9656  cnfcom  9657  cnfcom2lem  9658  cnfcom3lem  9660  fzen  13548  seqf1o  14058  wrdexg  14539  wrdnval  14560  pfxval  14689  pfxswrd  14721  splval  14766  ofccat  14984  climshftlem  15603  climshft  15605  climshft2  15611  caucvgr  15705  fsumrev  15808  hashdvds  16812  setsabs  17217  ressress  17285  firest  17463  prdsvscafval  17511  qusval  17574  xpsbas  17604  xpsadd  17606  xpsmul  17607  xpssca  17608  xpsvsca  17609  xpsless  17610  xpsle  17611  homfval  17726  comfval  17734  cicfval  17832  rescabs  17868  rescabs2  17869  resscat  17887  funcres2c  17938  ressffth  17975  fucbas  17998  fuccoval  18001  setchom  18115  catchom  18138  catcco  18140  estrchom  18161  funcestrcsetclem5  18178  funcsetcestrclem5  18193  evlf2val  18253  curf11  18260  curf12  18261  curf2val  18264  uncfval  18268  diagval  18274  hof2  18291  yonval  18295  resspos  18463  gsumval2a  18721  gsumval2  18722  mndpsuppss  18801  gsumwspan  18882  efmnd  18906  ghmqusnsglem1  19322  ghmqusnsglem2  19323  ghmqusnsg  19324  ghmquskerlem1  19325  ghmquskerco  19326  ghmquskerlem2  19327  ghmquskerlem3  19328  ghmqusker  19329  orbstafun  19353  orbstaval  19354  symgval  19413  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  20224  srgbinomlem3  20280  srgbinomlem4  20281  mulgass3  20404  rngcval  20670  rnghmsscmap2  20681  rnghmsscmap  20682  funcrngcsetc  20692  ringcval  20699  rhmsscmap2  20710  rhmsscmap  20711  funcringcsetc  20726  srhmsubclem3  20731  srhmsubc  20732  fldhmsubc  20836  lcomfsupp  20971  rmodislmodlem  20998  rmodislmod  20999  sraval  21244  srasca  21249  crngridl  21352  quscrng  21355  rhmqusnsg  21357  pzriprnglem11  21545  znval  21589  znzrhfo  21601  znunithash  21618  cygznlem2  21622  frobrhm  21629  pjfval  21760  pjpm  21762  frlmgsum  21826  frlmipval  21833  frlmphllem  21834  frlmphl  21835  frlmsslsp  21850  frlmup1  21852  gsumbagdiaglem  21985  psrass1lem  21987  rhmpsrlem1  21994  psrass1  22017  psrdi  22018  psrdir  22019  psrass23l  22020  psrascl  22032  mplval  22042  mplsubglem  22052  mplsubrglem  22057  mplmonmul  22091  mplcoe1  22092  opsrval  22101  psrbagev1  22132  psrbagev2  22133  evlslem6  22136  evlslem1  22137  evlsval  22141  evlsval3  22144  evlsvval  22145  evlsvvval  22148  evlcl  22157  evladdval  22158  evlmulval  22159  mpfconst  22164  mpff  22167  mpfaddcl  22168  mpfmulcl  22169  mpfind  22170  mhmcompl  22176  mhmcoaddmpl  22178  evlscl  22180  evlsexpval  22183  evlsaddval  22184  evlsmulval  22185  evlsevl  22187  selvcl  22195  mhpmulcl  22216  mhpaddcl  22218  psdcoef  22227  psdmplcl  22229  psdadd  22230  ply1lss  22260  gsumply1subr  22297  coe1add  22329  coe1tm  22338  coe1tmmul  22342  cply1mul  22361  ply1coe  22363  evl1expd  22410  pf1mpf  22417  pf1ind  22420  rhmmpl  22445  rhmply1vsca  22450  mamufv  22456  mamuass  22464  mamuvs1  22467  mamuvs2  22468  matgsum  22499  dmatmul  22559  scmatval  22566  scmatrhmval  22589  mvmulfv  22606  mavmulfv  22608  mavmulass  22611  marrepeval  22625  marepveval  22630  submaeval  22644  mdetrsca  22665  mdetunilem9  22682  mdetuni0  22683  gsummatr01lem3  22719  gsummatr01lem4  22720  gsummatr01  22721  smadiadetlem3  22730  cramerlem1  22749  mat2pmatmul  22793  m2cpminvid  22815  decpmatfsupp  22831  decpmatmullem  22833  decpmatmul  22834  decpmatmulsumfsupp  22835  pmatcollpw1lem1  22836  pmatcollpw3fi1lem1  22848  pmatcollpwscmatlem2  22852  pm2mpfval  22858  pm2mpf  22860  mply1topmatcllem  22865  mp2pm2mplem3  22870  mp2pm2mplem4  22871  pm2mpmhmlem1  22880  pm2mpmhmlem2  22881  pm2mp  22887  chfacfscmulfsupp  22921  chfacfscmulgsum  22922  chfacfpmmulfsupp  22925  chfacfpmmulgsum  22926  cpmidpmatlem3  22934  cpmadugsumlemB  22936  cpmadugsumlemC  22937  cpmadugsumlemF  22938  cayhamlem4  22950  xpstopnlem2  23873  fcfval  24095  tsmsxplem1  24215  tsmsxplem2  24216  tusval  24327  xpsdsfn  24439  xpsxmet  24442  xpsdsval  24443  xpsmet  24444  tmsval  24543  met1stc  24583  metuval  24611  cnmpopc  24992  pi1val  25101  pi1addf  25111  pi1addval  25112  pi1grplem  25113  rrxnm  25455  rrxcph  25456  rrxmval  25469  mbfmulc2  25727  mbfmul  25790  itg2mulclem  25810  ibladd  25885  itgadd  25889  itgabs  25899  bddmulibl  25903  dvmulf  26007  dvcmulf  26009  dvmptmul  26025  cmvth  26055  dvlip  26057  ftc1lem4  26103  mdegmullem  26140  coe1mul3  26161  r1pval  26220  plyco  26303  dgrcolem1  26335  elqaalem3  26387  taylpfval  26430  taylthlem2  26439  pserdvlem2  26493  advlogexp  26722  logtayl  26727  logccv  26730  dvcxp1  26807  dvcncxp1  26810  logbmpt  26855  logbfval  26857  relogbf  26858  dvatan  27002  cxp2lim  27043  cxploglim2  27045  lgamgulmlem2  27096  lgamgulm2  27102  lgamcvglem  27106  lgamf  27108  basellem7  27153  basellem8  27154  basellem9  27155  fsumdvdscom  27251  logexprlim  27291  dchrfi  27321  gausslemma2dlem2  27433  gausslemma2dlem3  27434  2lgslem1b  27458  chtppilimlem2  27540  chebbnd2  27543  chto1lb  27544  chpchtlim  27545  chpo1ub  27546  vmadivsum  27548  dchrisum0lem3  27585  mudivsum  27596  logdivsum  27599  log2sumbnd  27610  selberglem1  27611  selberg2lem  27616  selberg2  27617  selbergr  27634  negsval  28120  wlkp1  29882  cyclnumvtx  30002  wwlksnextsurj  30102  wwlksnextbij  30104  clwlkclwwlklem2a1  30196  clwlkclwwlkf1  30214  eupth2eucrct  30421  frgrncvvdeq  30513  numclwlk2lem2fv  30582  numclwwlk2lem3  30584  ofoprabco  32868  fsuppcurry1  32928  fsuppcurry2  32929  offinsupp1  32930  ressprs  33146  mntoval  33162  mgcoval  33166  mndlactf1  33206  mndlactfo  33207  mndractf1  33208  mndractfo  33209  mndlactf1o  33210  mndractf1o  33211  lmodvslmhm  33232  gsummulsubdishift2  33251  gsumwrd2dccat  33260  cycpmco2f1  33306  cycpmco2rn  33307  cycpmco2lem2  33309  cycpmco2lem3  33310  cycpmco2lem4  33311  cycpmco2lem5  33312  cycpmco2lem6  33313  cycpmco2  33315  conjga  33352  cntrval2  33353  fxpsubm  33354  fxpsubg  33355  fxpsubrg  33356  fxpsdrg  33357  archirngz  33371  archiabllem2a  33376  elrgspnlem1  33425  elrgspnlem2  33426  elrgspnsubrunlem2  33431  rlocval  33442  fracval  33493  quslmod  33546  quslmhm  33547  quslvec  33548  qustriv  33552  qustrivr  33553  unitprodclb  33577  nsgmgc  33600  nsgqusf1olem1  33601  nsgqusf1olem2  33602  nsgqusf1olem3  33603  lmhmqusker  33605  rhmquskerlem  33613  elrspunidl  33616  qsidomlem1  33641  qsidomlem2  33642  opprqusbas  33678  opprqusplusg  33679  opprqusmulr  33681  opprqus1r  33682  qsdrngilem  33684  qsdrngi  33685  rprmdvdsprod  33732  1arithidomlem1  33733  1arithidomlem2  33734  1arithidom  33735  1arithufdlem3  33744  dfufd2lem  33747  zringfrac  33752  evl1deg1  33774  evl1deg2  33775  evl1deg3  33776  ply1gsumz  33797  r1plmhm  33808  0mplrim  33813  selvply1rhmlema  33817  selvply1rhmlemb  33818  selvply1rhmlem1  33819  selvply1rhmlem3  33821  selvply1rhmlem4  33822  selvply1rhmlem5  33823  mplvrpmrhm  33846  psrgsum  33847  psrmonmul  33849  psrmonprod  33851  mplgsum  33852  splyval  33858  esplyfval1  33872  esplyfvaln  33873  vietadeg1  33877  resssra  33886  ply1degltdimlem  33921  ply1degltdim  33922  qusdimsum  33927  fedgmullem1  33928  fedgmullem2  33929  fedgmul  33930  lactlmhm  33933  fldgenfldext  33967  evls1fldgencl  33969  fldextrspunlsplem  33972  fldextrspundgdvdslem  33979  fldextrspundgdvds  33980  extdgfialglem1  33991  extdgfialglem2  33992  extdgfialg  33993  algextdeglem4  34019  algextdeglem6  34021  algextdeglem7  34022  submateq  34108  lmatcl  34115  mdetpmtr1  34122  madjusmdetlem1  34126  madjusmdetlem3  34128  qqhvval  34282  esumfzf  34368  esumpfinvallem  34373  esumpmono  34378  esummulc1  34380  esumcvg  34385  esumgect  34389  ofcval  34398  omssubadd  34599  sitgfval  34640  sitmcl  34650  sseqfv2  34693  cndprobval  34732  ballotlemfval  34789  ballotlemsv  34809  ballotlemsf1o  34813  ofcccat  34842  signsplypnf  34846  signsply0  34847  signstfval  34860  signshf  34884  reprpmtf1o  34922  reprdifc  34923  logdivsqrle  34946  hgt750lemg  34950  hgt750lema  34953  lpadval  34975  cvmliftlem8  35647  cvmliftphtlem  35672  fmla1  35742  gonarlem  35749  sategoelfvb  35774  mrsubval  35864  ellcsrspsn  35996  r1peuqusdeg1  35998  fwddifval  36517  knoppcnlem1  36936  knoppcnlem6  36941  unbdqndv2lem2  36953  poimirlem1  38125  poimirlem2  38126  poimirlem3  38127  poimirlem5  38129  poimirlem6  38130  poimirlem7  38131  poimirlem10  38134  poimirlem11  38135  poimirlem12  38136  poimirlem16  38140  poimirlem19  38143  poimirlem22  38146  poimirlem23  38147  broucube  38158  dvtan  38174  itg2addnc  38178  ibladdnc  38181  itgaddnc  38184  itgmulc2nclem2  38191  itgmulc2nc  38192  itgabsnc  38193  ftc1cnnclem  38195  ftc1anclem3  38199  ftc1anclem6  38202  ftc1anclem7  38203  ftc1anclem8  38204  dvasin  38208  dvacos  38209  dvreasin  38210  dvreacos  38211  areacirclem1  38212  areacirc  38217  fsumshftd  39581  hlrelat5N  40030  rhmzrhval  42594  aks6d1c1  42738  hashscontpow  42744  aks6d1c4  42746  aks6d1c2lem3  42748  aks6d1c2lem4  42749  aks6d1c2  42752  aks6d1c5lem0  42757  aks6d1c5lem3  42759  aks6d1c5lem2  42760  aks6d1c5  42761  sticksstones3  42770  sticksstones8  42775  sticksstones10  42777  sticksstones12a  42779  sticksstones12  42780  aks6d1c6lem1  42792  aks6d1c6lem2  42793  aks6d1c6lem3  42794  aks6d1c6lem4  42795  aks6d1c6isolem1  42796  aks6d1c6isolem2  42797  aks6d1c6isolem3  42798  aks6d1c6lem5  42799  aks6d1c7lem2  42803  unitscyglem1  42817  readvrec2  42975  readvrec  42976  readvcot  42978  frlmfzolen  43130  frlmfzoccat  43132  frlmvscadiccat  43133  evlsbagval  43173  evlselv  43176  fsuppind  43177  mhpind  43181  mhphflem  43183  prjspner  43206  prjspnvs  43207  prjspnfv01  43211  prjspner01  43212  prjspner1  43213  0prjspnrel  43214  prjcrv0  43220  mzpclall  43313  mzpsubst  43334  eldioph2  43348  rabdiophlem2  43384  irrapxlem1  43404  mzpcong  43554  mendlmod  43771  naddcnff  43944  relexpmulnn  44290  iunrelexpuztr  44300  mnringvald  44794  mnringmulrvald  44808  radcnvrat  44895  hashnzfzclim  44903  lhe4.4ex1a  44910  expgrowthi  44914  expgrowth  44916  bccval  44919  binomcxplemrat  44931  binomcxplemfrat  44932  binomcxplemradcnv  44933  binomcxplemdvbinom  44934  binomcxplemdvsum  44936  binomcxplemnotnn0  44937  unirnmap  45789  unirnmapsn  45795  ssmapsn  45797  iocopn  46101  icoopn  46106  divcnvg  46208  sumnnodd  46211  climsubmpt  46239  dvsinax  46492  fperdvper  46498  dvdivf  46501  dvnprodlem1  46525  itgsincmulx  46553  stoweidlem59  46638  etransclem4  46817  etransclem13  46826  etransclem25  46838  etransclem48  46861  rrxtopnfi  46866  sge0tsms  46959  elhoi  47121  ovnval2  47124  ovnval2b  47131  ovncvrrp  47143  ovn0lem  47144  ovncl  47146  ovnome  47152  hoidmvlelem2  47175  hoidmvlelem3  47176  hoidmvle  47179  ovnlecvr2  47189  ovncvr2  47190  ovnsubadd2lem  47224  ovnovollem1  47235  vonvolmbl  47240  iunhoiioolem  47254  vonioolem1  47259  vonioolem2  47260  vonicclem2  47263  smfresal  47367  smfres  47369  smfmullem4  47373  smfco  47381  adddmmbl  47412  muldmmbl  47414  chnsuslle  47462  nthrucw  47467  sinnpoly  47490  fmtno  48143  isubgruhgr  48495  grtriprop  48568  grtriclwlk3  48572  gpgvtx  48670  gpgiedg  48671  intopval  48829  clintopval  48831  rngchomALTV  48895  funcringcsetcALTV2lem5  48921  ringchomALTV  48929  funcringcsetclem5ALTV  48944  srhmsubcALTVlem2  48951  srhmsubcALTV  48952  fldhmsubcALTV  48960  zlmodzxzscm  48984  zlmodzxzadd  48985  rmsupp0  48995  domnmsuppn0  48996  rmsuppss  48997  ply1mulgsumlem3  49015  ply1mulgsumlem4  49016  ply1mulgsum  49017  dmatALTval  49027  lincop  49035  lincval  49036  linc1  49052  lincresunit3lem1  49106  fdivmpt  49167  fdivmptfv  49172  refdivmptfv  49173  digval  49225  2arymptfv  49277  2arymaptfo  49281  itcovalpclem1  49297  itcovalt2lem1  49302  ackvalsuc1mpt  49305  ackval1  49308  ackval2  49309  ackval3  49310  ackval42  49323  line2xlem  49380  upfval2  49803  swapfval  49888  tposcurf1  49925  tposcurf2val  49927  fucofvalg  49944  fuco112x  49958  fuco23  49967  fucoid  49974  fucocolem4  49982  prcofvalg  50002  prcof1  50014  opf2fval  50031  lanval  50245  ranval  50246