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

Theorem ovexd 6911
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
StepHypRef Expression
1 ovex 6909 . 2 (𝐴𝐹𝐵) ∈ V
21a1i 11 1 (𝜑 → (𝐴𝐹𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  Vcvv 3398  (class class class)co 6877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-nul 4990
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-sn 4378  df-pr 4380  df-uni 4638  df-iota 6067  df-fv 6112  df-ov 6880
This theorem is referenced by:  caofass  7164  caofdi  7166  caofdir  7167  caonncan  7168  mapsnend  8274  snmapen  8276  pw2eng  8308  mapen  8366  mapxpen  8368  mapdom2  8373  cantnfcl  8814  cantnflem1  8836  cnfcomlem  8846  cnfcom3lem  8850  cda1dif  9286  fzen  12584  seqf1o  13068  wrdnval  13549  splval  13729  cshwsexa  13797  ofccat  13936  climshftlem  14531  climshft  14533  climshft2  14539  caucvgr  14632  hashdvds  15700  setsabs  16116  ressress  16153  prdsvscafval  16348  qusval  16410  xpsbas  16442  xpsadd  16444  xpsmul  16445  xpssca  16446  xpsvsca  16447  xpsless  16448  xpsle  16449  homfval  16559  comfval  16567  cicfval  16664  rescabs  16700  rescabs2  16701  resscat  16719  fucbas  16827  fuccoval  16830  setchom  16937  catchom  16956  catcco  16958  estrchom  16974  funcestrcsetclem5  16992  funcsetcestrclem5  17007  evlf2val  17067  curf11  17074  curf12  17075  curf2val  17078  uncfval  17082  diagval  17088  hof2  17105  yonval  17109  gsumval2a  17487  gsumval2  17488  gsumwspan  17591  orbstafun  17948  orbstaval  17949  psgnvalii  18133  lsmhash  18322  frgpupval  18391  qusabl  18472  gsumval3  18512  gsumzaddlem  18525  gsummptshft  18540  telgsumfzslem  18590  telgsumfz  18592  telgsumfz0  18594  dpjval  18660  srgbinomlem3  18747  srgbinomlem4  18748  mulgass3  18842  lcomfsupp  19110  rmodislmodlem  19137  rmodislmod  19138  sraval  19388  srasca  19393  crngridl  19450  quscrng  19452  gsumbagdiaglem  19587  psrass1lem  19589  psrass1  19617  psrdi  19618  psrdir  19619  psrass23l  19620  mplval  19640  mplsubglem  19646  mplsubrglem  19651  mplmonmul  19676  mplcoe1  19677  opsrval  19686  psrbagev1  19721  evlslem6  19724  evlslem1  19726  evlsval  19730  mpfconst  19741  mpff  19744  mpfaddcl  19745  mpfmulcl  19746  mpfind  19747  ply1lss  19777  gsumply1subr  19815  coe1add  19845  coe1tm  19854  coe1tmmul  19858  cply1mul  19875  ply1coe  19877  evl1expd  19920  pf1mpf  19927  pf1ind  19930  znval  20094  znzrhfo  20106  znunithash  20123  cygznlem2  20127  pjfval  20264  pjpm  20266  frlmgsum  20325  frlmipval  20332  frlmphllem  20333  frlmphl  20334  frlmsslsp  20349  mamufv  20407  mamuass  20422  mamuvs1  20425  mamuvs2  20426  matgsum  20457  dmatmul  20518  scmatval  20525  scmatrhmval  20548  mvmulfv  20565  mavmulfv  20567  mavmulass  20570  marrepeval  20584  marepveval  20589  submaeval  20603  mdetrsca  20624  mdetunilem9  20641  mdetuni0  20642  gsummatr01lem3  20679  gsummatr01lem4  20680  gsummatr01  20681  smadiadetlem3  20690  cramerlem1  20710  mat2pmatmul  20753  m2cpminvid  20775  decpmatfsupp  20791  decpmatmullem  20793  decpmatmul  20794  decpmatmulsumfsupp  20795  pmatcollpw1lem1  20796  pmatcollpw3fi1lem1  20808  pmatcollpwscmatlem2  20812  pm2mpfval  20818  pm2mpf  20820  mply1topmatcllem  20825  mp2pm2mplem3  20830  mp2pm2mplem4  20831  pm2mpmhmlem1  20840  pm2mpmhmlem2  20841  pm2mp  20847  chfacfscmulfsupp  20881  chfacfscmulgsum  20882  chfacfpmmulfsupp  20885  chfacfpmmulgsum  20886  cpmidpmatlem3  20894  cpmadugsumlemB  20896  cpmadugsumlemC  20897  cpmadugsumlemF  20898  cayhamlem4  20910  xpstopnlem2  21832  fcfval  22054  tsmsxplem1  22173  tsmsxplem2  22174  tusval  22287  xpsdsfn  22399  xpsxmet  22402  xpsdsval  22403  xpsmet  22404  tmsval  22503  met1stc  22543  metuval  22571  cnmpt2pc  22944  pi1val  23053  pi1addf  23063  pi1addval  23064  pi1grplem  23065  rrxnm  23397  rrxcph  23398  rrxmval  23406  mbfmulc2  23650  mbfmul  23713  itg2mulclem  23733  ibladd  23807  itgadd  23811  itgabs  23821  bddmulibl  23825  dvmulf  23926  dvcmulf  23928  dvmptmul  23944  dvlip  23976  ftc1lem4  24022  mdegmullem  24058  coe1mul3  24079  r1pval  24136  plyco  24217  dgrcolem1  24249  elqaalem3  24296  taylpfval  24339  taylthlem2  24348  pserdvlem2  24402  advlogexp  24621  logtayl  24626  logccv  24629  dvcxp1  24701  dvcncxp1  24704  logbmpt  24746  logbfval  24748  relogbf  24749  dvatan  24882  cxp2lim  24923  cxploglim2  24925  lgamgulmlem2  24976  lgamgulm2  24982  lgamcvglem  24986  lgamf  24988  basellem7  25033  basellem8  25034  basellem9  25035  fsumdvdscom  25131  logexprlim  25170  dchrfi  25200  gausslemma2dlem2  25312  gausslemma2dlem3  25313  2lgslem1b  25337  chtppilimlem2  25383  chebbnd2  25386  chto1lb  25387  chpchtlim  25388  chpo1ub  25389  vmadivsum  25391  dchrisum0lem3  25428  mudivsum  25439  logdivsum  25442  log2sumbnd  25453  selberglem1  25454  selberg2lem  25459  selberg2  25460  selbergr  25477  wlkp1  26812  wwlksnextsur  27043  wwlksnextbij  27045  clwlkclwwlklem2a1  27141  clwlkclwwlkf1  27159  eupth2eucrct  27396  frgrncvvdeq  27490  numclwlk2lem2fv  27564  numclwwlk2lem3  27566  numclwlk2lem2fvOLD  27571  numclwwlk2lem3OLD  27573  ofoprabco  29797  ressprs  29986  resspos  29990  archirngz  30074  archiabllem2a  30079  submateq  30206  lmatcl  30213  mdetpmtr1  30220  madjusmdetlem1  30224  madjusmdetlem3  30226  qqhvval  30358  esumfzf  30462  esumpfinvallem  30467  esumpmono  30472  esummulc1  30474  esumcvg  30479  esumgect  30483  ofcval  30492  omssubadd  30693  sitgfval  30734  sitmcl  30744  sseqfv2  30787  cndprobval  30826  ballotlemfval  30882  ballotlemsv  30902  ballotlemsf1o  30906  ofcccat  30951  signsplypnf  30958  signsply0  30959  signstfval  30972  signshf  30996  reprpmtf1o  31035  reprdifc  31036  logdivsqrle  31059  hgt750lemg  31063  hgt750lema  31066  cvmliftlem8  31602  cvmliftphtlem  31627  mrsubval  31734  fwddifval  32595  knoppcnlem1  32805  knoppcnlem6  32810  unbdqndv2lem2  32823  poimirlem1  33725  poimirlem2  33726  poimirlem3  33727  poimirlem5  33729  poimirlem6  33730  poimirlem7  33731  poimirlem10  33734  poimirlem11  33735  poimirlem12  33736  poimirlem16  33740  poimirlem19  33743  poimirlem22  33746  poimirlem23  33747  broucube  33758  dvtan  33774  itg2addnc  33778  ibladdnc  33781  itgaddnc  33784  itgmulc2nclem2  33791  itgmulc2nc  33792  itgabsnc  33793  ftc1cnnclem  33797  ftc1anclem3  33801  ftc1anclem6  33804  ftc1anclem7  33805  ftc1anclem8  33806  dvasin  33810  dvacos  33811  dvreasin  33812  dvreacos  33813  areacirclem1  33814  areacirc  33819  fsumshftd  34733  hlrelat5N  35183  mzpclall  37793  mzpsubst  37814  eldioph2  37828  rabdiophlem2  37869  irrapxlem1  37889  mzpcong  38041  mendlmod  38265  relexpmulnn  38502  iunrelexpuztr  38512  radcnvrat  39014  hashnzfzclim  39022  lhe4.4ex1a  39029  expgrowthi  39033  expgrowth  39035  bccval  39038  binomcxplemrat  39050  binomcxplemfrat  39051  binomcxplemradcnv  39052  binomcxplemdvbinom  39053  binomcxplemdvsum  39055  binomcxplemnotnn0  39056  unirnmap  39888  unirnmapsn  39894  ssmapsn  39896  iocopn  40228  icoopn  40233  divcnvg  40340  sumnnodd  40343  climsubmpt  40373  dvsinax  40608  fperdvper  40614  dvdivf  40618  dvnprodlem1  40642  itgsincmulx  40670  stoweidlem59  40756  etransclem4  40935  etransclem13  40944  etransclem25  40956  etransclem48  40979  rrxtopnfi  40986  sge0tsms  41077  elhoi  41239  ovnval2  41242  ovnval2b  41249  ovncvrrp  41261  ovn0lem  41262  ovncl  41264  ovnome  41270  hoidmvlelem2  41293  hoidmvlelem3  41294  hoidmvle  41297  ovnlecvr2  41307  ovncvr2  41308  ovnsubadd2lem  41342  ovnovollem1  41353  vonvolmbl  41358  iunhoiioolem  41372  vonioolem1  41377  vonioolem2  41378  vonicclem2  41381  smfresal  41478  smfres  41480  smfmullem4  41484  smfco  41492  pfxval  41959  fmtno  42017  intopval  42407  clintopval  42409  rngcval  42531  rnghmsscmap2  42542  rnghmsscmap  42543  rngchomALTV  42554  funcrngcsetc  42567  ringcval  42577  rhmsscmap2  42588  rhmsscmap  42589  funcringcsetc  42604  funcringcsetcALTV2lem5  42609  ringchomALTV  42617  funcringcsetclem5ALTV  42632  srhmsubclem3  42644  srhmsubc  42645  fldhmsubc  42653  srhmsubcALTVlem2  42662  srhmsubcALTV  42663  fldhmsubcALTV  42671  zlmodzxzscm  42704  zlmodzxzadd  42705  rmsupp0  42718  domnmsuppn0  42719  rmsuppss  42720  ply1mulgsumlem3  42745  ply1mulgsumlem4  42746  ply1mulgsum  42747  dmatALTval  42758  lincop  42766  lincval  42767  linc1  42783  lincresunit3lem1  42837  fdivmpt  42903  fdivmptfv  42908  refdivmptfv  42909  digval  42961
  Copyright terms: Public domain W3C validator