Theorem ovexd 7397

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430  (class class class)co 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-sn 4569  df-pr 4571  df-uni 4852  df-iota 6450  df-fv 6502  df-ov 7365

This theorem is referenced by:  caofidlcan  7664  caofass  7666  caofdi  7668  caofdir  7669  caonncan  7670  suppofssd  8148  mapsnend  8978  snmapen  8980  pw2eng  9016  mapen  9074  mapxpen  9076  mapunen  9079  mapdom2  9081  cantnfcl  9583  cantnfle  9587  cantnflt  9588  cantnflt2  9589  cantnfp1lem2  9595  cantnfp1lem3  9596  cantnflem1b  9602  cantnflem1d  9604  cantnflem1  9605  cnfcomlem  9615  cnfcom  9616  cnfcom2lem  9617  cnfcom3lem  9619  fzen  13490  seqf1o  14000  wrdexg  14481  wrdnval  14502  pfxval  14631  pfxswrd  14663  splval  14708  ofccat  14926  climshftlem  15531  climshft  15533  climshft2  15539  caucvgr  15633  fsumrev  15736  hashdvds  16740  setsabs  17144  ressress  17212  firest  17390  prdsvscafval  17438  qusval  17501  xpsbas  17531  xpsadd  17533  xpsmul  17534  xpssca  17535  xpsvsca  17536  xpsless  17537  xpsle  17538  homfval  17653  comfval  17661  cicfval  17759  rescabs  17795  rescabs2  17796  resscat  17814  funcres2c  17865  ressffth  17902  fucbas  17925  fuccoval  17928  setchom  18042  catchom  18065  catcco  18067  estrchom  18088  funcestrcsetclem5  18105  funcsetcestrclem5  18120  evlf2val  18180  curf11  18187  curf12  18188  curf2val  18191  uncfval  18195  diagval  18201  hof2  18218  yonval  18222  resspos  18390  gsumval2a  18648  gsumval2  18649  mndpsuppss  18728  gsumwspan  18809  efmnd  18833  ghmqusnsglem1  19250  ghmqusnsglem2  19251  ghmqusnsg  19252  ghmquskerlem1  19253  ghmquskerco  19254  ghmquskerlem2  19255  ghmquskerlem3  19256  ghmqusker  19257  orbstafun  19281  orbstaval  19282  symgval  19341  psgnvalii  19479  lsmhash  19675  frgpupval  19744  qusabl  19835  gsumval3  19877  gsumreidx  19887  gsumzaddlem  19891  gsummptshft  19906  telgsumfzslem  19958  telgsumfz  19960  telgsumfz0  19962  dpjval  20028  prdsrngd  20152  srgbinomlem3  20204  srgbinomlem4  20205  mulgass3  20328  rngcval  20590  rnghmsscmap2  20601  rnghmsscmap  20602  funcrngcsetc  20612  ringcval  20619  rhmsscmap2  20630  rhmsscmap  20631  funcringcsetc  20646  srhmsubclem3  20651  srhmsubc  20652  fldhmsubc  20757  lcomfsupp  20892  rmodislmodlem  20919  rmodislmod  20920  sraval  21166  srasca  21171  crngridl  21274  quscrng  21277  rhmqusnsg  21279  pzriprnglem11  21485  znval  21529  znzrhfo  21541  znunithash  21558  cygznlem2  21562  frobrhm  21569  pjfval  21700  pjpm  21702  frlmgsum  21766  frlmipval  21773  frlmphllem  21774  frlmphl  21775  frlmsslsp  21790  frlmup1  21792  gsumbagdiaglem  21924  psrass1lem  21926  rhmpsrlem1  21933  psrass1  21956  psrdi  21957  psrdir  21958  psrass23l  21959  psrascl  21971  mplval  21981  mplsubglem  21991  mplsubrglem  21996  mplmonmul  22028  mplcoe1  22029  opsrval  22038  psrbagev1  22069  psrbagev2  22070  evlslem6  22073  evlslem1  22074  evlsval  22078  evlsval3  22081  evlsvval  22082  evlsvvval  22085  evlcl  22094  evladdval  22095  evlmulval  22096  mpfconst  22101  mpff  22104  mpfaddcl  22105  mpfmulcl  22106  mpfind  22107  mhpmulcl  22129  mhpaddcl  22131  psdcoef  22140  psdmplcl  22142  psdadd  22143  ply1lss  22174  gsumply1subr  22211  coe1add  22243  coe1tm  22252  coe1tmmul  22256  cply1mul  22275  ply1coe  22277  evl1expd  22324  pf1mpf  22331  pf1ind  22334  mhmcompl  22359  mhmcoaddmpl  22360  rhmmpl  22362  rhmply1vsca  22367  mamufv  22373  mamuass  22381  mamuvs1  22384  mamuvs2  22385  matgsum  22416  dmatmul  22476  scmatval  22483  scmatrhmval  22506  mvmulfv  22523  mavmulfv  22525  mavmulass  22528  marrepeval  22542  marepveval  22547  submaeval  22561  mdetrsca  22582  mdetunilem9  22599  mdetuni0  22600  gsummatr01lem3  22636  gsummatr01lem4  22637  gsummatr01  22638  smadiadetlem3  22647  cramerlem1  22666  mat2pmatmul  22710  m2cpminvid  22732  decpmatfsupp  22748  decpmatmullem  22750  decpmatmul  22751  decpmatmulsumfsupp  22752  pmatcollpw1lem1  22753  pmatcollpw3fi1lem1  22765  pmatcollpwscmatlem2  22769  pm2mpfval  22775  pm2mpf  22777  mply1topmatcllem  22782  mp2pm2mplem3  22787  mp2pm2mplem4  22788  pm2mpmhmlem1  22797  pm2mpmhmlem2  22798  pm2mp  22804  chfacfscmulfsupp  22838  chfacfscmulgsum  22839  chfacfpmmulfsupp  22842  chfacfpmmulgsum  22843  cpmidpmatlem3  22851  cpmadugsumlemB  22853  cpmadugsumlemC  22854  cpmadugsumlemF  22855  cayhamlem4  22867  xpstopnlem2  23790  fcfval  24012  tsmsxplem1  24132  tsmsxplem2  24133  tusval  24244  xpsdsfn  24356  xpsxmet  24359  xpsdsval  24360  xpsmet  24361  tmsval  24460  met1stc  24500  metuval  24528  cnmpopc  24909  pi1val  25018  pi1addf  25028  pi1addval  25029  pi1grplem  25030  rrxnm  25372  rrxcph  25373  rrxmval  25386  mbfmulc2  25644  mbfmul  25707  itg2mulclem  25727  ibladd  25802  itgadd  25806  itgabs  25816  bddmulibl  25820  dvmulf  25924  dvcmulf  25926  dvmptmul  25942  cmvth  25972  dvlip  25974  ftc1lem4  26020  mdegmullem  26057  coe1mul3  26078  r1pval  26137  plyco  26220  dgrcolem1  26252  elqaalem3  26302  taylpfval  26345  taylthlem2  26355  taylthlem2OLD  26356  pserdvlem2  26410  advlogexp  26636  logtayl  26641  logccv  26644  dvcxp1  26721  dvcncxp1  26724  logbmpt  26769  logbfval  26771  relogbf  26772  dvatan  26916  cxp2lim  26958  cxploglim2  26960  lgamgulmlem2  27011  lgamgulm2  27017  lgamcvglem  27021  lgamf  27023  basellem7  27068  basellem8  27069  basellem9  27070  fsumdvdscom  27166  logexprlim  27206  dchrfi  27236  gausslemma2dlem2  27348  gausslemma2dlem3  27349  2lgslem1b  27373  chtppilimlem2  27455  chebbnd2  27458  chto1lb  27459  chpchtlim  27460  chpo1ub  27461  vmadivsum  27463  dchrisum0lem3  27500  mudivsum  27511  logdivsum  27514  log2sumbnd  27525  selberglem1  27526  selberg2lem  27531  selberg2  27532  selbergr  27549  negsval  28035  wlkp1  29767  cyclnumvtx  29887  wwlksnextsurj  29987  wwlksnextbij  29989  clwlkclwwlklem2a1  30081  clwlkclwwlkf1  30099  eupth2eucrct  30306  frgrncvvdeq  30398  numclwlk2lem2fv  30467  numclwwlk2lem3  30469  ofoprabco  32756  fsuppcurry1  32816  fsuppcurry2  32817  offinsupp1  32818  ressprs  33045  mntoval  33061  mgcoval  33065  mndlactf1  33105  mndlactfo  33106  mndractf1  33107  mndractfo  33108  mndlactf1o  33109  mndractf1o  33110  lmodvslmhm  33130  gsummulsubdishift2  33149  gsumwrd2dccat  33158  cycpmco2f1  33204  cycpmco2rn  33205  cycpmco2lem2  33207  cycpmco2lem3  33208  cycpmco2lem4  33209  cycpmco2lem5  33210  cycpmco2lem6  33211  cycpmco2  33213  conjga  33250  cntrval2  33251  fxpsubm  33252  fxpsubg  33253  fxpsubrg  33254  fxpsdrg  33255  archirngz  33269  archiabllem2a  33274  elrgspnlem1  33322  elrgspnlem2  33323  elrgspnsubrunlem2  33328  rlocval  33339  fracval  33384  quslmod  33437  quslmhm  33438  quslvec  33439  qustriv  33443  qustrivr  33444  unitprodclb  33468  nsgmgc  33491  nsgqusf1olem1  33492  nsgqusf1olem2  33493  nsgqusf1olem3  33494  lmhmqusker  33496  rhmquskerlem  33504  elrspunidl  33507  qsidomlem1  33531  qsidomlem2  33532  opprqusbas  33567  opprqusplusg  33568  opprqusmulr  33570  opprqus1r  33571  qsdrngilem  33573  qsdrngi  33574  rprmdvdsprod  33613  1arithidomlem1  33614  1arithidomlem2  33615  1arithidom  33616  1arithufdlem3  33625  dfufd2lem  33628  zringfrac  33633  evl1deg1  33655  evl1deg2  33656  evl1deg3  33657  ply1gsumz  33678  r1plmhm  33689  mplvrpmrhm  33710  psrgsum  33711  psrmonmul  33713  psrmonprod  33715  mplgsum  33716  splyval  33722  esplyfval1  33736  esplyfvaln  33737  vietadeg1  33741  resssra  33750  ply1degltdimlem  33786  ply1degltdim  33787  qusdimsum  33792  fedgmullem1  33793  fedgmullem2  33794  fedgmul  33795  lactlmhm  33798  fldgenfldext  33832  evls1fldgencl  33834  fldextrspunlsplem  33837  fldextrspundgdvdslem  33844  fldextrspundgdvds  33845  extdgfialglem1  33856  extdgfialglem2  33857  extdgfialg  33858  algextdeglem4  33884  algextdeglem6  33886  algextdeglem7  33887  submateq  33973  lmatcl  33980  mdetpmtr1  33987  madjusmdetlem1  33991  madjusmdetlem3  33993  qqhvval  34147  esumfzf  34233  esumpfinvallem  34238  esumpmono  34243  esummulc1  34245  esumcvg  34250  esumgect  34254  ofcval  34263  omssubadd  34464  sitgfval  34505  sitmcl  34515  sseqfv2  34558  cndprobval  34597  ballotlemfval  34654  ballotlemsv  34674  ballotlemsf1o  34678  ofcccat  34707  signsplypnf  34714  signsply0  34715  signstfval  34728  signshf  34752  reprpmtf1o  34790  reprdifc  34791  logdivsqrle  34814  hgt750lemg  34818  hgt750lema  34821  lpadval  34840  cvmliftlem8  35494  cvmliftphtlem  35519  fmla1  35589  gonarlem  35596  sategoelfvb  35621  mrsubval  35711  ellcsrspsn  35843  r1peuqusdeg1  35845  fwddifval  36364  knoppcnlem1  36773  knoppcnlem6  36778  unbdqndv2lem2  36790  poimirlem1  37962  poimirlem2  37963  poimirlem3  37964  poimirlem5  37966  poimirlem6  37967  poimirlem7  37968  poimirlem10  37971  poimirlem11  37972  poimirlem12  37973  poimirlem16  37977  poimirlem19  37980  poimirlem22  37983  poimirlem23  37984  broucube  37995  dvtan  38011  itg2addnc  38015  ibladdnc  38018  itgaddnc  38021  itgmulc2nclem2  38028  itgmulc2nc  38029  itgabsnc  38030  ftc1cnnclem  38032  ftc1anclem3  38036  ftc1anclem6  38039  ftc1anclem7  38040  ftc1anclem8  38041  dvasin  38045  dvacos  38046  dvreasin  38047  dvreacos  38048  areacirclem1  38049  areacirc  38054  fsumshftd  39418  hlrelat5N  39867  rhmzrhval  42431  aks6d1c1  42575  hashscontpow  42581  aks6d1c4  42583  aks6d1c2lem3  42585  aks6d1c2lem4  42586  aks6d1c2  42589  aks6d1c5lem0  42594  aks6d1c5lem3  42596  aks6d1c5lem2  42597  aks6d1c5  42598  sticksstones3  42607  sticksstones8  42612  sticksstones10  42614  sticksstones12a  42616  sticksstones12  42617  aks6d1c6lem1  42629  aks6d1c6lem2  42630  aks6d1c6lem3  42631  aks6d1c6lem4  42632  aks6d1c6isolem1  42633  aks6d1c6isolem2  42634  aks6d1c6isolem3  42635  aks6d1c6lem5  42636  aks6d1c7lem2  42640  unitscyglem1  42654  readvrec2  42813  readvrec  42814  readvcot  42816  frlmfzolen  42968  frlmfzoccat  42970  frlmvscadiccat  42971  evlscl  43019  evlsbagval  43022  evlsexpval  43023  evlsaddval  43024  evlsmulval  43025  evlsevl  43027  selvcl  43036  evlselv  43040  fsuppind  43043  mhpind  43047  mhphflem  43049  prjspner  43072  prjspnvs  43073  prjspnfv01  43077  prjspner01  43078  prjspner1  43079  0prjspnrel  43080  prjcrv0  43086  mzpclall  43179  mzpsubst  43200  eldioph2  43214  rabdiophlem2  43254  irrapxlem1  43274  mzpcong  43424  mendlmod  43641  naddcnff  43814  relexpmulnn  44160  iunrelexpuztr  44170  mnringvald  44664  mnringmulrvald  44678  radcnvrat  44765  hashnzfzclim  44773  lhe4.4ex1a  44780  expgrowthi  44784  expgrowth  44786  bccval  44789  binomcxplemrat  44801  binomcxplemfrat  44802  binomcxplemradcnv  44803  binomcxplemdvbinom  44804  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  unirnmap  45661  unirnmapsn  45667  ssmapsn  45669  iocopn  45974  icoopn  45979  divcnvg  46081  sumnnodd  46084  climsubmpt  46112  dvsinax  46365  fperdvper  46371  dvdivf  46374  dvnprodlem1  46398  itgsincmulx  46426  stoweidlem59  46511  etransclem4  46690  etransclem13  46699  etransclem25  46711  etransclem48  46734  rrxtopnfi  46739  sge0tsms  46832  elhoi  46994  ovnval2  46997  ovnval2b  47004  ovncvrrp  47016  ovn0lem  47017  ovncl  47019  ovnome  47025  hoidmvlelem2  47048  hoidmvlelem3  47049  hoidmvle  47052  ovnlecvr2  47062  ovncvr2  47063  ovnsubadd2lem  47097  ovnovollem1  47108  vonvolmbl  47113  iunhoiioolem  47127  vonioolem1  47132  vonioolem2  47133  vonicclem2  47136  smfresal  47240  smfres  47242  smfmullem4  47246  smfco  47254  adddmmbl  47285  muldmmbl  47287  chnsuslle  47333  nthrucw  47338  sinnpoly  47357  fmtno  48010  isubgruhgr  48362  grtriprop  48435  grtriclwlk3  48439  gpgvtx  48537  gpgiedg  48538  intopval  48696  clintopval  48698  rngchomALTV  48762  funcringcsetcALTV2lem5  48788  ringchomALTV  48796  funcringcsetclem5ALTV  48811  srhmsubcALTVlem2  48818  srhmsubcALTV  48819  fldhmsubcALTV  48827  zlmodzxzscm  48851  zlmodzxzadd  48852  rmsupp0  48862  domnmsuppn0  48863  rmsuppss  48864  ply1mulgsumlem3  48882  ply1mulgsumlem4  48883  ply1mulgsum  48884  dmatALTval  48894  lincop  48902  lincval  48903  linc1  48919  lincresunit3lem1  48973  fdivmpt  49034  fdivmptfv  49039  refdivmptfv  49040  digval  49092  2arymptfv  49144  2arymaptfo  49148  itcovalpclem1  49164  itcovalt2lem1  49169  ackvalsuc1mpt  49172  ackval1  49175  ackval2  49176  ackval3  49177  ackval42  49190  line2xlem  49247  upfval2  49670  swapfval  49755  tposcurf1  49792  tposcurf2val  49794  fucofvalg  49811  fuco112x  49825  fuco23  49834  fucoid  49841  fucocolem4  49849  prcofvalg  49869  prcof1  49881  opf2fval  49898  lanval  50112  ranval  50113