MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovexd Structured version   Visualization version   GIF version

Theorem ovexd 6665
Description: The result of an operation is a set (common case). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Assertion
Ref Expression
ovexd (𝜑 → (𝐴𝐹𝐵) ∈ V)

Proof of Theorem ovexd
StepHypRef Expression
1 ovex 6663 . 2 (𝐴𝐹𝐵) ∈ V
21a1i 11 1 (𝜑 → (𝐴𝐹𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  Vcvv 3195  (class class class)co 6635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-nul 4780
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-sn 4169  df-pr 4171  df-uni 4428  df-iota 5839  df-fv 5884  df-ov 6638
This theorem is referenced by:  caofass  6916  caofdi  6918  caofdir  6919  caonncan  6920  map1  8021  pw2eng  8051  mapen  8109  mapxpen  8111  mapdom2  8116  cantnfcl  8549  cantnflem1  8571  cnfcomlem  8581  cnfcom3lem  8585  cda1dif  8983  fzen  12343  seqf1o  12825  wrdnval  13318  splval  13483  cshwsexa  13551  ofccat  13689  climshftlem  14286  climshft  14288  climshft2  14294  caucvgr  14387  hashdvds  15461  setsabs  15883  ressress  15919  prdsvscafval  16121  qusval  16183  xpsbas  16215  xpsadd  16217  xpsmul  16218  xpssca  16219  xpsvsca  16220  xpsless  16221  xpsle  16222  homfval  16333  comfval  16341  cicfval  16438  rescabs  16474  rescabs2  16475  resscat  16493  fucbas  16601  fuccoval  16604  setchom  16711  catchom  16730  catcco  16732  estrchom  16748  funcestrcsetclem5  16765  funcsetcestrclem5  16780  evlf2val  16840  curf11  16847  curf12  16848  curf2val  16851  uncfval  16855  diagval  16861  hof2  16878  yonval  16882  gsumval2a  17260  gsumval2  17261  gsumwspan  17364  orbstafun  17725  orbstaval  17726  psgnvalii  17910  lsmhash  18099  frgpupval  18168  qusabl  18249  gsumval3  18289  gsumzaddlem  18302  gsummptshft  18317  telgsumfzslem  18366  telgsumfz  18368  telgsumfz0  18370  dpjval  18436  srgbinomlem3  18523  srgbinomlem4  18524  mulgass3  18618  lcomfsupp  18884  rmodislmodlem  18911  rmodislmod  18912  sraval  19157  srasca  19162  crngridl  19219  quscrng  19221  gsumbagdiaglem  19356  psrass1lem  19358  psrass1  19386  psrdi  19387  psrdir  19388  psrass23l  19389  mplval  19409  mplsubglem  19415  mplsubrglem  19420  mplmonmul  19445  mplcoe1  19446  opsrval  19455  psrbagev1  19491  evlslem6  19494  evlslem1  19496  evlsval  19500  mpfconst  19511  mpff  19514  mpfaddcl  19515  mpfmulcl  19516  mpfind  19517  ply1lss  19547  gsumply1subr  19585  coe1add  19615  coe1tm  19624  coe1tmmul  19628  cply1mul  19645  ply1coe  19647  evl1expd  19690  pf1mpf  19697  pf1ind  19700  znval  19864  znzrhfo  19877  znunithash  19894  cygznlem2  19898  pjfval  20031  pjpm  20033  frlmgsum  20092  frlmipval  20099  frlmphllem  20100  frlmphl  20101  frlmsslsp  20116  mamufv  20174  mamuass  20189  mamuvs1  20192  mamuvs2  20193  matgsum  20224  dmatmul  20284  scmatval  20291  scmatrhmval  20314  mvmulfv  20331  mavmulfv  20333  mavmulass  20336  marrepeval  20350  marepveval  20355  submaeval  20369  mdetrsca  20390  mdetunilem9  20407  mdetuni0  20408  gsummatr01lem3  20444  gsummatr01lem4  20445  gsummatr01  20446  smadiadetlem3  20455  cramerlem1  20474  mat2pmatmul  20517  m2cpminvid  20539  decpmatfsupp  20555  decpmatmullem  20557  decpmatmul  20558  decpmatmulsumfsupp  20559  pmatcollpw1lem1  20560  pmatcollpw3fi1lem1  20572  pmatcollpwscmatlem2  20576  pm2mpfval  20582  pm2mpf  20584  mply1topmatcllem  20589  mp2pm2mplem3  20594  mp2pm2mplem4  20595  pm2mpmhmlem1  20604  pm2mpmhmlem2  20605  pm2mp  20611  chfacfscmulfsupp  20645  chfacfscmulgsum  20646  chfacfpmmulfsupp  20649  chfacfpmmulgsum  20650  cpmidpmatlem3  20658  cpmadugsumlemB  20660  cpmadugsumlemC  20661  cpmadugsumlemF  20662  cayhamlem4  20674  xpstopnlem2  21595  fcfval  21818  tsmsxplem1  21937  tsmsxplem2  21938  tusval  22051  xpsdsfn  22163  xpsxmet  22166  xpsdsval  22167  xpsmet  22168  tmsval  22267  met1stc  22307  metuval  22335  cnmpt2pc  22708  pi1val  22818  pi1addf  22828  pi1addval  22829  pi1grplem  22830  rrxnm  23160  rrxcph  23161  rrxmval  23169  mbfmulc2  23411  mbfmul  23474  itg2mulclem  23494  ibladd  23568  itgadd  23572  itgabs  23582  bddmulibl  23586  dvmulf  23687  dvcmulf  23689  dvmptmul  23705  dvlip  23737  ftc1lem4  23783  mdegmullem  23819  coe1mul3  23840  r1pval  23897  plyco  23978  dgrcolem1  24010  elqaalem3  24057  taylpfval  24100  taylthlem2  24109  pserdvlem2  24163  advlogexp  24382  logtayl  24387  logccv  24390  dvcxp1  24462  dvcncxp1  24465  logbmpt  24507  logbfval  24509  relogbf  24510  dvatan  24643  cxp2lim  24684  cxploglim2  24686  lgamgulmlem2  24737  lgamgulm2  24743  lgamcvglem  24747  lgamf  24749  basellem7  24794  basellem8  24795  basellem9  24796  fsumdvdscom  24892  logexprlim  24931  dchrfi  24961  gausslemma2dlem2  25073  gausslemma2dlem3  25074  2lgslem1b  25098  chtppilimlem2  25144  chebbnd2  25147  chto1lb  25148  chpchtlim  25149  chpo1ub  25150  vmadivsum  25152  dchrisum0lem3  25189  mudivsum  25200  logdivsum  25203  log2sumbnd  25214  selberglem1  25215  selberg2lem  25220  selberg2  25221  selbergr  25238  wlkp1  26559  wwlksnextsur  26776  wwlksnextbij  26778  clwlkclwwlklem2a1  26874  eupth2eucrct  27057  frgrncvvdeq  27153  numclwlk2lem2fv  27208  numclwwlk2lem3  27210  ofoprabco  29438  ressprs  29629  resspos  29633  archirngz  29717  archiabllem2a  29722  submateq  29849  lmatcl  29856  mdetpmtr1  29863  madjusmdetlem1  29867  madjusmdetlem3  29869  qqhvval  30001  esumfzf  30105  esumpfinvallem  30110  esumpmono  30115  esummulc1  30117  esumcvg  30122  esumgect  30126  ofcval  30135  omssubadd  30336  sitgfval  30377  sitmcl  30387  sseqfv2  30430  cndprobval  30469  ballotlemfval  30525  ballotlemsv  30545  ballotlemsf1o  30549  ofcccat  30594  signsplypnf  30601  signsply0  30602  signstfval  30615  signshf  30639  reprpmtf1o  30678  reprdifc  30679  logdivsqrle  30702  hgt750lemg  30706  hgt750lema  30709  cvmliftlem8  31248  cvmliftphtlem  31273  mrsubval  31380  fwddifval  32244  knoppcnlem1  32458  knoppcnlem6  32463  unbdqndv2lem2  32476  poimirlem1  33381  poimirlem2  33382  poimirlem3  33383  poimirlem5  33385  poimirlem6  33386  poimirlem7  33387  poimirlem10  33390  poimirlem11  33391  poimirlem12  33392  poimirlem16  33396  poimirlem19  33399  poimirlem22  33402  poimirlem23  33403  broucube  33414  dvtan  33431  itg2addnc  33435  ibladdnc  33438  itgaddnc  33441  itgmulc2nclem2  33448  itgmulc2nc  33449  itgabsnc  33450  ftc1cnnclem  33454  ftc1anclem3  33458  ftc1anclem6  33461  ftc1anclem7  33462  ftc1anclem8  33463  dvasin  33467  dvacos  33468  dvreasin  33469  dvreacos  33470  areacirclem1  33471  areacirc  33476  fsumshftd  34056  hlrelat5N  34506  mzpclall  37109  mzpsubst  37130  eldioph2  37144  rabdiophlem2  37185  irrapxlem1  37205  mzpcong  37358  mendlmod  37582  relexpmulnn  37820  iunrelexpuztr  37830  radcnvrat  38333  hashnzfzclim  38341  lhe4.4ex1a  38348  expgrowthi  38352  expgrowth  38354  bccval  38357  binomcxplemrat  38369  binomcxplemfrat  38370  binomcxplemradcnv  38371  binomcxplemdvbinom  38372  binomcxplemdvsum  38374  binomcxplemnotnn0  38375  mapsnend  39207  unirnmap  39216  unirnmapsn  39222  ssmapsn  39224  iocopn  39549  icoopn  39554  divcnvg  39659  sumnnodd  39662  climsubmpt  39692  dvsinax  39890  fperdvper  39896  dvdivf  39900  dvnprodlem1  39924  itgsincmulx  39953  stoweidlem59  40039  etransclem4  40218  etransclem13  40227  etransclem25  40239  etransclem48  40262  rrxtopnfi  40269  sge0tsms  40360  elhoi  40519  ovnval2  40522  ovnval2b  40529  ovncvrrp  40541  ovn0lem  40542  ovncl  40544  ovnome  40550  hoidmvlelem2  40573  hoidmvlelem3  40574  hoidmvle  40577  ovnlecvr2  40587  ovncvr2  40588  ovnsubadd2lem  40622  ovnovollem1  40633  vonvolmbl  40638  iunhoiioolem  40652  vonioolem1  40657  vonioolem2  40658  vonicclem2  40661  smfresal  40758  smfres  40760  smfmullem4  40764  smfco  40772  pfxval  41148  fmtno  41206  intopval  41603  clintopval  41605  rngcval  41727  rnghmsscmap2  41738  rnghmsscmap  41739  rngchomALTV  41750  funcrngcsetc  41763  ringcval  41773  rhmsscmap2  41784  rhmsscmap  41785  funcringcsetc  41800  funcringcsetcALTV2lem5  41805  ringchomALTV  41813  funcringcsetclem5ALTV  41828  srhmsubclem3  41840  srhmsubc  41841  fldhmsubc  41849  srhmsubcALTVlem2  41858  srhmsubcALTV  41859  fldhmsubcALTV  41867  zlmodzxzscm  41900  zlmodzxzadd  41901  rmsupp0  41914  domnmsuppn0  41915  rmsuppss  41916  ply1mulgsumlem3  41941  ply1mulgsumlem4  41942  ply1mulgsum  41943  dmatALTval  41954  lincop  41962  lincval  41963  linc1  41979  lincresunit3lem1  42033  fdivmpt  42099  fdivmptfv  42104  refdivmptfv  42105  digval  42157
  Copyright terms: Public domain W3C validator