Theorem ovexd 7444

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450  (class class class)co 7409

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5260

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6484  df-fv 6536  df-ov 7412

This theorem is used by:  caofidlcan  7715  caofass  7717  caofdi  7719  caofdir  7720  caonncan  7721  suppofssd  8199  mapsnend  9043  snmapen  9045  pw2eng  9081  mapen  9139  mapxpen  9141  mapunen  9144  mapdom2  9146  cantnfcl  9646  cantnfle  9650  cantnflt  9651  cantnflt2  9652  cantnfp1lem2  9658  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1d  9667  cantnflem1  9668  cnfcomlem  9678  cnfcom  9679  cnfcom2lem  9680  cnfcom3lem  9682  fzen  13628  seqf1o  14140  wrdexg  14622  wrdnval  14643  pfxval  14776  pfxswrd  14808  splval  14853  s3rex  15054  s3rexrd  15055  ofccat  15075  climshftlem  15694  climshft  15696  climshft2  15702  caucvgr  15796  fsumrev  15898  hashdvds  16899  setsabs  17304  ressress  17372  firest  17550  prdsvscafval  17598  qusval  17661  xpsbas  17691  xpsadd  17693  xpsmul  17694  xpssca  17695  xpsvsca  17696  xpsless  17697  xpsle  17698  homfval  17813  comfval  17821  cicfval  17919  rescabs  17955  rescabs2  17956  resscat  17974  funcres2c  18025  ressffth  18062  fucbas  18085  fuccoval  18088  setchom  18202  catchom  18225  catcco  18227  estrchom  18248  funcestrcsetclem5  18265  funcsetcestrclem5  18280  evlf2val  18340  curf11  18347  curf12  18348  curf2val  18351  uncfval  18355  diagval  18361  hof2  18378  yonval  18382  resspos  18550  gsumval2a  18821  gsumval2  18822  mndpsuppss  18906  gsumwspan  18989  efmnd  19013  qustriv  19343  qustrivr  19344  ghmqusnsglem1  19441  ghmqusnsglem2  19442  ghmqusnsg  19443  ghmquskerlem1  19444  ghmquskerco  19445  ghmquskerlem2  19446  ghmquskerlem3  19447  ghmqusker  19448  orbstafun  19472  orbstaval  19473  symgval  19532  psgnvalii  19670  lsmhash  19866  frgpupval  19935  qusabl  20026  gsumval3  20068  gsumreidx  20078  gsumzaddlem  20082  gsummptshft  20097  telgsumfzslem  20149  telgsumfz  20151  telgsumfz0  20153  dpjval  20219  prdsrngd  20345  srgbinomlem3  20401  srgbinomlem4  20402  mulgass3  20530  rngcval  20817  rnghmsscmap2  20828  rnghmsscmap  20829  funcrngcsetc  20839  ringcval  20846  rhmsscmap2  20857  rhmsscmap  20858  funcringcsetc  20873  srhmsubclem3  20878  srhmsubc  20879  fldhmsubc  20989  lcomfsupp  21124  rmodislmodlem  21151  rmodislmod  21152  sraval  21397  srasca  21402  crngridl  21522  quscrng  21526  rhmqusnsg  21528  qsidomlem1  21583  qsidomlem2  21584  pzriprnglem11  21744  znval  21788  znzrhfo  21800  znunithash  21817  cygznlem2  21821  frobrhm  21828  pjfval  21959  pjpm  21961  frlmgsum  22025  frlmipval  22032  frlmphllem  22033  frlmphl  22034  frlmsslsp  22049  frlmup1  22051  gsumbagdiaglem  22186  psrass1lem  22188  rhmpsrlem1  22195  psrass1  22218  psrdi  22219  psrdir  22220  psrass23l  22221  psrascl  22233  mplval  22243  mplsubglem  22253  mplsubrglem  22258  mplmonmul  22292  mplcoe1  22293  opsrval  22302  psrbagev1  22333  psrbagev2  22334  evlslem6  22337  evlslem1  22338  evlsval  22342  evlsval3  22345  evlsvval  22346  evlsvvval  22349  evlcl  22358  evladdval  22359  evlmulval  22360  mpfconst  22365  mpff  22368  mpfaddcl  22369  mpfmulcl  22370  mpfind  22371  mhmcompl  22377  mhmcoaddmpl  22379  evlscl  22381  evlsexpval  22384  evlsaddval  22385  evlsmulval  22386  evlsevl  22388  selvcl  22396  mhpmulcl  22417  mhpaddcl  22419  psdcoef  22428  psdmplcl  22430  psdadd  22431  ply1lss  22461  gsumply1subr  22498  coe1add  22530  coe1tm  22539  coe1tmmul  22543  cply1mul  22561  ply1coe  22563  evl1expd  22610  pf1mpf  22617  pf1ind  22620  rhmmpl  22645  rhmply1vsca  22650  mamufv  22656  mamuass  22664  mamuvs1  22667  mamuvs2  22668  matgsum  22699  dmatmul  22759  scmatval  22766  scmatrhmval  22789  mvmulfv  22806  mavmulfv  22808  mavmulass  22811  marrepeval  22825  marepveval  22830  submaeval  22844  mdetrsca  22865  mdetunilem9  22882  mdetuni0  22883  gsummatr01lem3  22919  gsummatr01lem4  22920  gsummatr01  22921  smadiadetlem3  22930  cramerlem1  22952  mat2pmatmul  22996  m2cpminvid  23018  decpmatfsupp  23034  decpmatmullem  23036  decpmatmul  23037  decpmatmulsumfsupp  23038  pmatcollpw1lem1  23039  pmatcollpw3fi1lem1  23051  pmatcollpwscmatlem2  23055  pm2mpfval  23061  pm2mpf  23063  mply1topmatcllem  23068  mp2pm2mplem3  23073  mp2pm2mplem4  23074  pm2mpmhmlem1  23083  pm2mpmhmlem2  23084  pm2mp  23090  chfacfscmulfsupp  23124  chfacfscmulgsum  23125  chfacfpmmulfsupp  23128  chfacfpmmulgsum  23129  cpmidpmatlem3  23137  cpmadugsumlemB  23139  cpmadugsumlemC  23140  cpmadugsumlemF  23141  cayhamlem4  23153  xpstopnlem2  24077  fcfval  24299  tsmsxplem1  24419  tsmsxplem2  24420  tusval  24531  xpsdsfn  24643  xpsxmet  24646  xpsdsval  24647  xpsmet  24648  tmsval  24747  met1stc  24787  metuval  24815  cnmpopc  25196  pi1val  25305  pi1addf  25315  pi1addval  25316  pi1grplem  25317  rrxnm  25659  rrxcph  25660  rrxmval  25673  mbfmulc2  25931  mbfmul  25994  itg2mulclem  26014  ibladd  26088  itgadd  26092  itgabs  26102  bddmulibl  26106  dvmulf  26210  dvcmulf  26212  dvmptmul  26228  cmvth  26258  dvlip  26260  ftc1lem4  26306  mdegmullem  26343  coe1mul3  26364  r1pval  26423  plyco  26507  dgrcolem1  26539  elqaalem3  26593  taylpfval  26641  taylthlem2  26650  pserdvlem2  26704  advlogexp  26932  logtayl  26937  logccv  26940  dvcxp1  27017  dvcncxp1  27020  logbmpt  27065  logbfval  27067  relogbf  27068  dvatan  27212  cxp2lim  27253  cxploglim2  27255  lgamgulmlem2  27306  lgamgulm2  27312  lgamcvglem  27316  lgamf  27318  basellem7  27363  basellem8  27364  basellem9  27365  fsumdvdscom  27461  logexprlim  27501  dchrfi  27531  gausslemma2dlem2  27643  gausslemma2dlem3  27644  2lgslem1b  27668  chtppilimlem2  27750  chebbnd2  27753  chto1lb  27754  chpchtlim  27755  chpo1ub  27756  vmadivsum  27758  dchrisum0lem3  27795  mudivsum  27806  logdivsum  27809  log2sumbnd  27820  selberglem1  27821  selberg2lem  27826  selberg2  27827  selbergr  27844  negsval  28330  cgrabasimass  29297  angmgmval  29313  wlkp1  30179  cyclnumvtx  30307  wwlksnextsurj  30408  wwlksnextbij  30410  clwlkclwwlklem2a1  30502  clwlkclwwlkf1  30520  eupth2eucrct  30737  frgrncvvdeq  30829  numclwlk2lem2fv  30898  numclwwlk2lem3  30900  ofoprabco  33177  fsuppcurry1  33235  fsuppcurry2  33236  offinsupp1  33237  ressprs  33446  mntoval  33462  mgcoval  33466  mndlactf1  33506  mndlactfo  33507  mndractf1  33508  mndractfo  33509  mndlactf1o  33510  mndractf1o  33511  lmodvslmhm  33530  gsummulsubdishift2  33549  gsumwrd2dccat  33558  cycpmco2f1  33604  cycpmco2rn  33605  cycpmco2lem2  33607  cycpmco2lem3  33608  cycpmco2lem4  33609  cycpmco2lem5  33610  cycpmco2lem6  33611  cycpmco2  33613  conjga  33650  cntrval2  33651  fxpsubm  33652  fxpsubg  33653  fxpsubrg  33654  fxpsdrg  33655  archirngz  33669  archiabllem2a  33674  elrgspnlem1  33722  elrgspnlem2  33723  elrgspnsubrunlem2  33728  rlocval  33739  fracval  33785  quslmod  33838  quslmhm  33839  quslvec  33840  unitprodclb  33863  nsgmgc  33882  nsgqusf1olem1  33883  nsgqusf1olem2  33884  nsgqusf1olem3  33885  lmhmqusker  33887  rhmquskerlem  33894  elrspunidl  33897  opprqusbas  33931  opprqusplusg  33932  opprqusmulr  33934  opprqus1r  33935  qsdrngilem  33937  qsdrngi  33938  rprmdvdsprod  33985  1arithidomlem1  33986  1arithidomlem2  33987  1arithidom  33988  1arithufdlem3  33997  dfufd2lem  34000  zringfrac  34005  evl1deg1  34027  evl1deg2  34028  evl1deg3  34029  ply1gsumz  34050  r1plmhm  34060  0mplrim  34065  selvply1rhmlema  34069  selvply1rhmlemb  34070  selvply1rhmlem1  34071  selvply1rhmlem3  34073  selvply1rhmlem4  34074  selvply1rhmlem5  34075  mplvrpmrhm  34098  psrgsum  34099  psrmonmul  34101  psrmonprod  34103  mplgsum  34104  splyval  34110  esplyfval1  34124  esplyfvaln  34125  vietadeg1  34129  resssra  34138  ply1degltdimlem  34173  ply1degltdim  34174  qusdimsum  34179  fedgmullem1  34180  fedgmullem2  34181  fedgmul  34182  lactlmhm  34185  fldgenfldext  34219  evls1fldgencl  34221  fldextrspunlsplem  34224  fldextrspundgdvdslem  34231  fldextrspundgdvds  34232  extdgfialglem1  34243  extdgfialglem2  34244  algextdeglem4  34271  algextdeglem6  34273  algextdeglem7  34274  submateq  34360  lmatcl  34367  mdetpmtr1  34374  madjusmdetlem1  34378  madjusmdetlem3  34380  qqhvval  34534  esumfzf  34620  esumpfinvallem  34625  esumpmono  34630  esummulc1  34632  esumcvg  34637  esumgect  34641  ofcval  34650  omssubadd  34852  sitgfval  34893  sitmcl  34903  sseqfv2  34946  cndprobval  34985  ballotlemfval  35042  ballotlemsv  35062  ballotlemsf1o  35066  ofcccat  35095  signsplypnf  35099  signsply0  35100  signstfval  35113  signshf  35137  reprpmtf1o  35175  reprdifc  35176  logdivsqrle  35199  hgt750lemg  35203  hgt750lema  35206  lpadval  35228  cvmliftlem8  35972  cvmliftphtlem  35997  fmla1  36067  gonarlem  36074  sategoelfvb  36099  mrsubval  36189  ellcsrspsn  36321  r1peuqusdeg1  36323  fwddifval  36843  knoppcnlem1  37275  knoppcnlem6  37280  unbdqndv2lem2  37292  poimirlem1  38453  poimirlem2  38454  poimirlem3  38455  poimirlem5  38457  poimirlem6  38458  poimirlem7  38459  poimirlem10  38462  poimirlem11  38463  poimirlem12  38464  poimirlem16  38468  poimirlem19  38471  poimirlem22  38474  poimirlem23  38475  broucube  38486  dvtan  38502  itg2addnc  38506  ibladdnc  38509  itgaddnc  38512  itgmulc2nclem2  38519  itgmulc2nc  38520  itgabsnc  38521  ftc1cnnclem  38523  ftc1anclem3  38527  ftc1anclem6  38530  ftc1anclem7  38531  ftc1anclem8  38532  dvasin  38536  dvacos  38537  dvreasin  38538  dvreacos  38539  areacirclem1  38540  areacirc  38545  fsumshftd  39923  hlrelat5N  40372  rhmzrhval  42936  aks6d1c1  43080  hashscontpow  43086  aks6d1c4  43088  aks6d1c2lem3  43090  aks6d1c2lem4  43091  aks6d1c2  43094  aks6d1c5lem0  43099  aks6d1c5lem3  43101  aks6d1c5lem2  43102  aks6d1c5  43103  sticksstones3  43112  sticksstones8  43117  sticksstones10  43119  sticksstones12a  43121  sticksstones12  43122  aks6d1c6lem1  43134  aks6d1c6lem2  43135  aks6d1c6lem3  43136  aks6d1c6lem4  43137  aks6d1c6isolem1  43138  aks6d1c6isolem2  43139  aks6d1c6isolem3  43140  aks6d1c6lem5  43141  aks6d1c7lem2  43145  unitscyglem1  43159  readvrec2  43334  readvrec  43335  readvcot  43337  frlmfzolen  43489  frlmfzoccat  43491  frlmvscadiccat  43492  evlsbagval  43530  evlselv  43533  fsuppind  43534  mhpind  43538  mhphflem  43540  prjspner  43563  prjspnvs  43564  prjspnfv01  43568  prjspner01  43569  prjspner1  43570  0prjspnrel  43571  prjcrv0  43577  mzpclall  43670  mzpsubst  43691  eldioph2  43705  rabdiophlem2  43741  irrapxlem1  43761  mzpcong  43911  mendlmod  44128  naddcnff  44301  relexpmulnn  44647  iunrelexpuztr  44657  mnringvald  45149  mnringmulrvald  45163  radcnvrat  45236  hashnzfzclim  45244  lhe4.4ex1a  45251  expgrowthi  45255  expgrowth  45257  bccval  45260  binomcxplemrat  45272  binomcxplemfrat  45273  binomcxplemradcnv  45274  binomcxplemdvbinom  45275  binomcxplemdvsum  45277  binomcxplemnotnn0  45278  unirnmap  46136  unirnmapsn  46142  ssmapsn  46144  iocopn  46448  icoopn  46453  divcnvg  46555  sumnnodd  46558  climsubmpt  46586  dvsinax  46839  fperdvper  46845  dvdivf  46848  dvnprodlem1  46872  itgsincmulx  46900  stoweidlem59  46985  etransclem4  47164  etransclem13  47173  etransclem25  47185  etransclem48  47208  rrxtopnfi  47213  sge0tsms  47306  elhoi  47468  ovnval2  47471  ovnval2b  47478  ovncvrrp  47490  ovn0lem  47491  ovncl  47493  ovnome  47499  hoidmvlelem2  47522  hoidmvlelem3  47523  hoidmvle  47526  ovnlecvr2  47536  ovncvr2  47537  ovnsubadd2lem  47571  ovnovollem1  47582  vonvolmbl  47587  iunhoiioolem  47601  vonioolem1  47606  vonioolem2  47607  vonicclem2  47610  smfresal  47714  smfres  47716  smfmullem4  47720  smfco  47728  adddmmbl  47759  muldmmbl  47761  chnsuslle  47807  fmtno  48530  isubgruhgr  48882  grtriprop  48955  grtriclwlk3  48959  gpgvtx  49057  gpgiedg  49058  intopval  49215  clintopval  49217  rngchomALTV  49281  funcringcsetcALTV2lem5  49307  ringchomALTV  49315  funcringcsetclem5ALTV  49330  srhmsubcALTVlem2  49337  srhmsubcALTV  49338  fldhmsubcALTV  49346  zlmodzxzscm  49385  zlmodzxzadd  49386  rmsupp0  49396  domnmsuppn0  49397  rmsuppss  49398  ply1mulgsumlem3  49416  ply1mulgsumlem4  49417  ply1mulgsum  49418  dmatALTval  49428  lincop  49436  lincval  49437  linc1  49453  lincresunit3lem1  49507  fdivmpt  49568  fdivmptfv  49573  refdivmptfv  49574  digval  49626  2arymptfv  49678  2arymaptfo  49682  itcovalpclem1  49698  itcovalt2lem1  49703  ackvalsuc1mpt  49706  ackval1  49709  ackval2  49710  ackval3  49711  ackval42  49724  line2xlem  49781  upfval2  50201  swapfval  50286  tposcurf1  50323  tposcurf2val  50325  fucofvalg  50342  fuco112x  50356  fuco23  50365  fucoid  50372  fucocolem4  50380  prcofvalg  50400  prcof1  50412  opf2fval  50429  lanval  50643  ranval  50644  crosspdot0lem  50879  veroquadgsumlem  50899