Theorem ovexd 7475

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454  (class class class)co 7440

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591  df-uni 4871  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  caofidlcan  7752  caofass  7754  caofdi  7756  caofdir  7757  caonncan  7758  suppofssd  8245  mapsnend  9089  snmapen  9091  pw2eng  9127  mapen  9185  mapxpen  9187  mapunen  9190  mapdom2  9192  cantnfcl  9692  cantnfle  9696  cantnflt  9697  cantnflt2  9698  cantnfp1lem2  9704  cantnfp1lem3  9705  cantnflem1b  9711  cantnflem1d  9713  cantnflem1  9714  cnfcomlem  9724  cnfcom  9725  cnfcom2lem  9726  cnfcom3lem  9728  fzen  13698  seqf1o  14210  wrdexg  14693  wrdnval  14714  s1mapd  14780  pfxval  14848  pfxswrd  14880  splval  14925  s2mapd  15067  s3rex  15127  s3rexrd  15128  ofccat  15148  climshftlem  15767  climshft  15769  climshft2  15775  caucvgr  15869  fsumrev  15971  hashdvds  16978  setsabs  17383  ressress  17451  firest  17629  prdsvscafval  17677  qusval  17740  xpsbas  17770  xpsadd  17772  xpsmul  17773  xpssca  17774  xpsvsca  17775  xpsless  17776  xpsle  17777  homfval  17892  comfval  17900  cicfval  17998  rescabs  18034  rescabs2  18035  resscat  18053  funcres2c  18104  ressffth  18141  fucbas  18164  fuccoval  18167  setchom  18281  catchom  18304  catcco  18306  estrchom  18327  funcestrcsetclem5  18344  funcsetcestrclem5  18359  evlf2val  18419  curf11  18426  curf12  18427  curf2val  18430  uncfval  18434  diagval  18440  hof2  18457  yonval  18461  resspos  18629  gsumval2a  18900  gsumval2  18901  mndpsuppss  18985  gsumwspan  19068  efmnd  19092  qustriv  19422  qustrivr  19423  ghmqusnsglem1  19521  ghmqusnsglem2  19522  ghmqusnsg  19523  ghmquskerlem1  19524  ghmquskerco  19525  ghmquskerlem2  19526  ghmquskerlem3  19527  ghmqusker  19528  orbstafun  19552  orbstaval  19553  symgval  19612  psgnvalii  19750  lsmhash  19946  frgpupval  20015  qusabl  20106  gsumval3  20148  gsumreidx  20158  gsumzaddlem  20162  gsummptshft  20177  telgsumfzslem  20229  telgsumfz  20231  telgsumfz0  20233  dpjval  20299  prdsrngd  20425  srgbinomlem3  20481  srgbinomlem4  20482  mulgass3  20610  rngcval  20897  rnghmsscmap2  20908  rnghmsscmap  20909  funcrngcsetc  20919  ringcval  20926  rhmsscmap2  20937  rhmsscmap  20938  funcringcsetc  20953  srhmsubclem3  20958  srhmsubc  20959  fldhmsubc  21069  lcomfsupp  21204  rmodislmodlem  21231  rmodislmod  21232  sraval  21477  srasca  21482  crngridl  21602  quscrng  21606  rhmqusnsg  21608  qsidomlem1  21663  qsidomlem2  21664  pzriprnglem11  21824  znval  21868  znzrhfo  21880  znunithash  21897  cygznlem2  21901  frobrhm  21908  pjfval  22039  pjpm  22041  frlmgsum  22105  frlmipval  22112  frlmphllem  22113  frlmphl  22114  frlmsslsp  22129  frlmup1  22131  gsumbagdiaglem  22266  psrass1lem  22268  rhmpsrlem1  22275  psrass1  22298  psrdi  22299  psrdir  22300  psrass23l  22301  psrascl  22313  mplval  22323  mplsubglem  22333  mplsubrglem  22338  mplmonmul  22372  mplcoe1  22373  opsrval  22382  psrbagev1  22413  psrbagev2  22414  evlslem6  22417  evlslem1  22418  evlsval  22422  evlsval3  22425  evlsvval  22426  evlsvvval  22429  evlcl  22438  evladdval  22439  evlmulval  22440  mpfconst  22445  mpff  22448  mpfaddcl  22449  mpfmulcl  22450  mpfind  22451  mhmcompl  22457  mhmcoaddmpl  22459  evlscl  22461  evlsexpval  22464  evlsaddval  22465  evlsmulval  22466  evlsevl  22468  selvcl  22476  mhpmulcl  22497  mhpaddcl  22499  psdcoef  22508  psdmplcl  22510  psdadd  22511  ply1lss  22541  gsumply1subr  22578  coe1add  22610  coe1tm  22619  coe1tmmul  22623  cply1mul  22641  ply1coe  22643  evl1expd  22690  pf1mpf  22697  pf1ind  22700  rhmmpl  22725  rhmply1vsca  22730  mamufv  22736  mamuass  22744  mamuvs1  22747  mamuvs2  22748  matgsum  22779  dmatmul  22839  scmatval  22846  scmatrhmval  22869  mvmulfv  22886  mavmulfv  22888  mavmulass  22891  marrepeval  22905  marepveval  22910  submaeval  22924  mdetrsca  22945  mdetunilem9  22962  mdetuni0  22963  gsummatr01lem3  22999  gsummatr01lem4  23000  gsummatr01  23001  smadiadetlem3  23010  cramerlem1  23032  mat2pmatmul  23076  m2cpminvid  23098  decpmatfsupp  23114  decpmatmullem  23116  decpmatmul  23117  decpmatmulsumfsupp  23118  pmatcollpw1lem1  23119  pmatcollpw3fi1lem1  23131  pmatcollpwscmatlem2  23135  pm2mpfval  23141  pm2mpf  23143  mply1topmatcllem  23148  mp2pm2mplem3  23153  mp2pm2mplem4  23154  pm2mpmhmlem1  23163  pm2mpmhmlem2  23164  pm2mp  23170  chfacfscmulfsupp  23204  chfacfscmulgsum  23205  chfacfpmmulfsupp  23208  chfacfpmmulgsum  23209  cpmidpmatlem3  23217  cpmadugsumlemB  23219  cpmadugsumlemC  23220  cpmadugsumlemF  23221  cayhamlem4  23233  xpstopnlem2  24157  fcfval  24379  tsmsxplem1  24499  tsmsxplem2  24500  tusval  24611  xpsdsfn  24723  xpsxmet  24726  xpsdsval  24727  xpsmet  24728  tmsval  24827  met1stc  24867  metuval  24895  cnmpopc  25276  pi1val  25385  pi1addf  25395  pi1addval  25396  pi1grplem  25397  rrxnm  25739  rrxcph  25740  rrxmval  25753  mbfmulc2  26011  mbfmul  26074  itg2mulclem  26094  ibladd  26168  itgadd  26172  itgabs  26182  bddmulibl  26186  dvmulf  26290  dvcmulf  26292  dvmptmul  26308  cmvth  26338  dvlip  26340  ftc1lem4  26386  mdegmullem  26423  coe1mul3  26444  r1pval  26503  plyco  26587  dgrcolem1  26619  elqaalem3  26671  taylpfval  26719  taylthlem2  26728  pserdvlem2  26782  advlogexp  27010  logtayl  27015  logccv  27018  dvcxp1  27095  dvcncxp1  27098  logbmpt  27143  logbfval  27145  relogbf  27146  dvatan  27290  cxp2lim  27331  cxploglim2  27333  lgamgulmlem2  27384  lgamgulm2  27390  lgamcvglem  27394  lgamf  27396  basellem7  27441  basellem8  27442  basellem9  27443  fsumdvdscom  27539  logexprlim  27579  dchrfi  27609  gausslemma2dlem2  27721  gausslemma2dlem3  27722  2lgslem1b  27746  chtppilimlem2  27828  chebbnd2  27831  chto1lb  27832  chpchtlim  27833  chpo1ub  27834  vmadivsum  27836  dchrisum0lem3  27873  mudivsum  27884  logdivsum  27887  log2sumbnd  27898  selberglem1  27899  selberg2lem  27904  selberg2  27905  selbergr  27922  negsval  28438  cgrabasimass  29405  angmgmval  29421  wlkp1  30287  cyclnumvtx  30415  wwlksnextsurj  30516  wwlksnextbij  30518  clwlkclwwlklem2a1  30610  clwlkclwwlkf1  30628  eupth2eucrct  30845  frgrncvvdeq  30937  numclwlk2lem2fv  31006  numclwwlk2lem3  31008  ofoprabco  33327  fsuppcurry1  33383  fsuppcurry2  33384  offinsupp1  33385  ressprs  33594  mntoval  33610  mgcoval  33614  mndlactf1  33654  mndlactfo  33655  mndractf1  33656  mndractfo  33657  mndlactf1o  33658  mndractf1o  33659  lmodvslmhm  33678  gsummulsubdishift2  33697  gsumwrd2dccat  33706  cycpmco2f1  33752  cycpmco2rn  33753  cycpmco2lem2  33755  cycpmco2lem3  33756  cycpmco2lem4  33757  cycpmco2lem5  33758  cycpmco2lem6  33759  cycpmco2  33761  conjga  33798  cntrval2  33799  fxpsubm  33800  fxpsubg  33801  fxpsubrg  33802  fxpsdrg  33803  archirngz  33817  archiabllem2a  33822  elrgspnlem1  33870  elrgspnlem2  33871  elrgspnsubrunlem2  33876  rlocval  33887  fracval  33933  quslmod  33986  quslmhm  33987  quslvec  33988  unitprodclb  34011  nsgmgc  34030  nsgqusf1olem1  34031  nsgqusf1olem2  34032  nsgqusf1olem3  34033  lmhmqusker  34035  rhmquskerlem  34042  elrspunidl  34045  opprqusbas  34079  opprqusplusg  34080  opprqusmulr  34082  opprqus1r  34083  qsdrngilem  34085  qsdrngi  34086  rprmdvdsprod  34133  1arithidomlem1  34134  1arithidomlem2  34135  1arithidom  34136  1arithufdlem3  34145  dfufd2lem  34148  zringfrac  34153  evl1deg1  34175  evl1deg2  34176  evl1deg3  34177  ply1gsumz  34198  r1plmhm  34208  0mplrim  34213  selvply1rhmlema  34217  selvply1rhmlemb  34218  selvply1rhmlem1  34219  selvply1rhmlem3  34221  selvply1rhmlem4  34222  selvply1rhmlem5  34223  mplvrpmrhm  34246  psrgsum  34247  psrmonmul  34249  psrmonprod  34251  mplgsum  34252  splyval  34258  esplyfval1  34272  esplyfvaln  34273  vietadeg1  34277  resssra  34286  ply1degltdimlem  34321  ply1degltdim  34322  qusdimsum  34327  fedgmullem1  34328  fedgmullem2  34329  fedgmul  34330  lactlmhm  34333  fldgenfldext  34367  evls1fldgencl  34369  fldextrspunlsplem  34372  fldextrspundgdvdslem  34379  fldextrspundgdvds  34380  extdgfialglem1  34391  extdgfialglem2  34392  algextdeglem4  34419  algextdeglem6  34421  algextdeglem7  34422  submateq  34508  lmatcl  34515  mdetpmtr1  34522  madjusmdetlem1  34526  madjusmdetlem3  34528  qqhvval  34682  esumfzf  34768  esumpfinvallem  34773  esumpmono  34778  esummulc1  34780  esumcvg  34785  esumgect  34789  ofcval  34798  omssubadd  34999  sitgfval  35040  sitmcl  35050  sseqfv2  35093  cndprobval  35132  ballotlemfval  35189  ballotlemsv  35209  ballotlemsf1o  35213  ofcccat  35242  signsplypnf  35246  signsply0  35247  signstfval  35260  signshf  35284  reprpmtf1o  35322  reprdifc  35323  logdivsqrle  35346  hgt750lemg  35350  hgt750lema  35353  lpadval  35375  j0le  36018  k3n0j0lt  36019  jltaleph  36025  cvmliftlem8  36223  cvmliftphtlem  36248  fmla1  36318  gonarlem  36325  sategoelfvb  36350  mrsubval  36440  ellcsrspsn  36572  r1peuqusdeg1  36574  fwddifval  37104  knoppcnlem1  37536  knoppcnlem6  37541  unbdqndv2lem2  37553  poimirlem1  38730  poimirlem2  38731  poimirlem3  38732  poimirlem5  38734  poimirlem6  38735  poimirlem7  38736  poimirlem10  38739  poimirlem11  38740  poimirlem12  38741  poimirlem16  38745  poimirlem19  38748  poimirlem22  38751  poimirlem23  38752  broucube  38763  dvtan  38779  itg2addnc  38783  ibladdnc  38786  itgaddnc  38789  itgmulc2nclem2  38796  itgmulc2nc  38797  itgabsnc  38798  ftc1cnnclem  38800  ftc1anclem3  38804  ftc1anclem6  38807  ftc1anclem7  38808  ftc1anclem8  38809  dvasin  38813  dvacos  38814  dvreasin  38815  dvreacos  38816  areacirclem1  38817  areacirc  38822  fsumshftd  40200  hlrelat5N  40649  rhmzrhval  43213  aks6d1c1  43357  hashscontpow  43363  aks6d1c4  43365  aks6d1c2lem3  43367  aks6d1c2lem4  43368  aks6d1c2  43371  aks6d1c5lem0  43376  aks6d1c5lem3  43378  aks6d1c5lem2  43379  aks6d1c5  43380  sticksstones3  43389  sticksstones8  43394  sticksstones10  43396  sticksstones12a  43398  sticksstones12  43399  aks6d1c6lem1  43411  aks6d1c6lem2  43412  aks6d1c6lem3  43413  aks6d1c6lem4  43414  aks6d1c6isolem1  43415  aks6d1c6isolem2  43416  aks6d1c6isolem3  43417  aks6d1c6lem5  43418  aks6d1c7lem2  43422  unitscyglem1  43436  readvrec2  43603  readvrec  43604  readvcot  43606  frlmfzolen  43761  frlmfzoccat  43763  frlmvscadiccat  43764  evlsbagval  43805  evlselv  43808  fsuppind  43809  mhpind  43813  mhphflem  43815  prjspner  43838  prjspnvs  43839  frlmnzcoordex  43843  frlmnzcoordcl2  43847  frlmnzcoordsca  43849  prjspnnormval  43850  prjspnnorm  43852  0prjspnrel  43854  prjcrv0  43860  mzpclall  43929  mzpsubst  43950  eldioph2  43964  rabdiophlem2  44000  irrapxlem1  44020  mzpcong  44170  mendlmod  44381  naddcnff  44554  relexpmulnn  44899  iunrelexpuztr  44909  mnringvald  45401  mnringmulrvald  45415  radcnvrat  45488  hashnzfzclim  45496  lhe4.4ex1a  45503  expgrowthi  45507  expgrowth  45509  bccval  45512  binomcxplemrat  45524  binomcxplemfrat  45525  binomcxplemradcnv  45526  binomcxplemdvbinom  45527  binomcxplemdvsum  45529  binomcxplemnotnn0  45530  unirnmap  46424  unirnmapsn  46430  ssmapsn  46432  iocopn  46735  icoopn  46740  divcnvg  46842  sumnnodd  46845  climsubmpt  46873  dvsinax  47126  fperdvper  47132  dvdivf  47135  dvnprodlem1  47159  itgsincmulx  47187  stoweidlem59  47272  etransclem4  47451  etransclem13  47460  etransclem25  47472  etransclem48  47495  rrxtopnfi  47500  sge0tsms  47593  elhoi  47755  ovnval2  47758  ovnval2b  47765  ovncvrrp  47777  ovn0lem  47778  ovncl  47780  ovnome  47786  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvle  47813  ovnlecvr2  47823  ovncvr2  47824  ovnsubadd2lem  47858  ovnovollem1  47869  vonvolmbl  47874  iunhoiioolem  47888  vonioolem1  47893  vonioolem2  47894  vonicclem2  47897  smfresal  48001  smfres  48003  smfmullem4  48007  smfco  48015  adddmmbl  48046  muldmmbl  48048  chnsuslle  48094  fmtno  48817  isubgruhgr  49169  grtriprop  49242  grtriclwlk3  49246  gpgvtx  49344  gpgiedg  49345  intopval  49502  clintopval  49504  rngchomALTV  49568  funcringcsetcALTV2lem5  49594  ringchomALTV  49602  funcringcsetclem5ALTV  49617  srhmsubcALTVlem2  49624  srhmsubcALTV  49625  fldhmsubcALTV  49633  zlmodzxzscm  49672  zlmodzxzadd  49673  rmsupp0  49683  domnmsuppn0  49684  rmsuppss  49685  ply1mulgsumlem3  49703  ply1mulgsumlem4  49704  ply1mulgsum  49705  dmatALTval  49715  lincop  49723  lincval  49724  linc1  49740  lincresunit3lem1  49794  fdivmpt  49855  fdivmptfv  49860  refdivmptfv  49861  digval  49913  2arymptfv  49965  2arymaptfo  49969  itcovalpclem1  49985  itcovalt2lem1  49990  ackvalsuc1mpt  49993  ackval1  49996  ackval2  49997  ackval3  49998  ackval42  50011  prelrrx2bd  50029  line2xlem  50068  elovmpoeq  50183  upfval2  50496  swapfval  50587  tposcurf1  50624  tposcurf2val  50626  fucofvalg  50643  fuco112x  50657  fuco23  50666  fucoid  50673  fucocolem4  50681  prcofvalg  50714  prcof1  50726  opf2fval  50743  lanval  51005  ranval  51006  crosspdot0lem  51241  veroquadgsumlem  51261