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

Theorem ovexd 6720
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 6718 . 2 (𝐴𝐹𝐵) ∈ V
21a1i 11 1 (𝜑 → (𝐴𝐹𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  Vcvv 3231  (class class class)co 6690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-sn 4211  df-pr 4213  df-uni 4469  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  caofass  6973  caofdi  6975  caofdir  6976  caonncan  6977  map1  8077  pw2eng  8107  mapen  8165  mapxpen  8167  mapdom2  8172  cantnfcl  8602  cantnflem1  8624  cnfcomlem  8634  cnfcom3lem  8638  cda1dif  9036  fzen  12396  seqf1o  12882  wrdnval  13367  splval  13548  cshwsexa  13616  ofccat  13754  climshftlem  14349  climshft  14351  climshft2  14357  caucvgr  14450  hashdvds  15527  setsabs  15949  ressress  15985  prdsvscafval  16187  qusval  16249  xpsbas  16281  xpsadd  16283  xpsmul  16284  xpssca  16285  xpsvsca  16286  xpsless  16287  xpsle  16288  homfval  16399  comfval  16407  cicfval  16504  rescabs  16540  rescabs2  16541  resscat  16559  fucbas  16667  fuccoval  16670  setchom  16777  catchom  16796  catcco  16798  estrchom  16814  funcestrcsetclem5  16831  funcsetcestrclem5  16846  evlf2val  16906  curf11  16913  curf12  16914  curf2val  16917  uncfval  16921  diagval  16927  hof2  16944  yonval  16948  gsumval2a  17326  gsumval2  17327  gsumwspan  17430  orbstafun  17790  orbstaval  17791  psgnvalii  17975  lsmhash  18164  frgpupval  18233  qusabl  18314  gsumval3  18354  gsumzaddlem  18367  gsummptshft  18382  telgsumfzslem  18431  telgsumfz  18433  telgsumfz0  18435  dpjval  18501  srgbinomlem3  18588  srgbinomlem4  18589  mulgass3  18683  lcomfsupp  18951  rmodislmodlem  18978  rmodislmod  18979  sraval  19224  srasca  19229  crngridl  19286  quscrng  19288  gsumbagdiaglem  19423  psrass1lem  19425  psrass1  19453  psrdi  19454  psrdir  19455  psrass23l  19456  mplval  19476  mplsubglem  19482  mplsubrglem  19487  mplmonmul  19512  mplcoe1  19513  opsrval  19522  psrbagev1  19558  evlslem6  19561  evlslem1  19563  evlsval  19567  mpfconst  19578  mpff  19581  mpfaddcl  19582  mpfmulcl  19583  mpfind  19584  ply1lss  19614  gsumply1subr  19652  coe1add  19682  coe1tm  19691  coe1tmmul  19695  cply1mul  19712  ply1coe  19714  evl1expd  19757  pf1mpf  19764  pf1ind  19767  znval  19931  znzrhfo  19944  znunithash  19961  cygznlem2  19965  pjfval  20098  pjpm  20100  frlmgsum  20159  frlmipval  20166  frlmphllem  20167  frlmphl  20168  frlmsslsp  20183  mamufv  20241  mamuass  20256  mamuvs1  20259  mamuvs2  20260  matgsum  20291  dmatmul  20351  scmatval  20358  scmatrhmval  20381  mvmulfv  20398  mavmulfv  20400  mavmulass  20403  marrepeval  20417  marepveval  20422  submaeval  20436  mdetrsca  20457  mdetunilem9  20474  mdetuni0  20475  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  smadiadetlem3  20522  cramerlem1  20541  mat2pmatmul  20584  m2cpminvid  20606  decpmatfsupp  20622  decpmatmullem  20624  decpmatmul  20625  decpmatmulsumfsupp  20626  pmatcollpw1lem1  20627  pmatcollpw3fi1lem1  20639  pmatcollpwscmatlem2  20643  pm2mpfval  20649  pm2mpf  20651  mply1topmatcllem  20656  mp2pm2mplem3  20661  mp2pm2mplem4  20662  pm2mpmhmlem1  20671  pm2mpmhmlem2  20672  pm2mp  20678  chfacfscmulfsupp  20712  chfacfscmulgsum  20713  chfacfpmmulfsupp  20716  chfacfpmmulgsum  20717  cpmidpmatlem3  20725  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cayhamlem4  20741  xpstopnlem2  21662  fcfval  21884  tsmsxplem1  22003  tsmsxplem2  22004  tusval  22117  xpsdsfn  22229  xpsxmet  22232  xpsdsval  22233  xpsmet  22234  tmsval  22333  met1stc  22373  metuval  22401  cnmpt2pc  22774  pi1val  22883  pi1addf  22893  pi1addval  22894  pi1grplem  22895  rrxnm  23225  rrxcph  23226  rrxmval  23234  mbfmulc2  23475  mbfmul  23538  itg2mulclem  23558  ibladd  23632  itgadd  23636  itgabs  23646  bddmulibl  23650  dvmulf  23751  dvcmulf  23753  dvmptmul  23769  dvlip  23801  ftc1lem4  23847  mdegmullem  23883  coe1mul3  23904  r1pval  23961  plyco  24042  dgrcolem1  24074  elqaalem3  24121  taylpfval  24164  taylthlem2  24173  pserdvlem2  24227  advlogexp  24446  logtayl  24451  logccv  24454  dvcxp1  24526  dvcncxp1  24529  logbmpt  24571  logbfval  24573  relogbf  24574  dvatan  24707  cxp2lim  24748  cxploglim2  24750  lgamgulmlem2  24801  lgamgulm2  24807  lgamcvglem  24811  lgamf  24813  basellem7  24858  basellem8  24859  basellem9  24860  fsumdvdscom  24956  logexprlim  24995  dchrfi  25025  gausslemma2dlem2  25137  gausslemma2dlem3  25138  2lgslem1b  25162  chtppilimlem2  25208  chebbnd2  25211  chto1lb  25212  chpchtlim  25213  chpo1ub  25214  vmadivsum  25216  dchrisum0lem3  25253  mudivsum  25264  logdivsum  25267  log2sumbnd  25278  selberglem1  25279  selberg2lem  25284  selberg2  25285  selbergr  25302  wlkp1  26634  wwlksnextsur  26863  wwlksnextbij  26865  clwlkclwwlklem2a1  26958  eupth2eucrct  27195  frgrncvvdeq  27289  numclwlk2lem2fv  27358  numclwwlk2lem3  27360  numclwlk2lem2fvOLD  27365  numclwwlk2lem3OLD  27367  ofoprabco  29592  ressprs  29783  resspos  29787  archirngz  29871  archiabllem2a  29876  submateq  30003  lmatcl  30010  mdetpmtr1  30017  madjusmdetlem1  30021  madjusmdetlem3  30023  qqhvval  30155  esumfzf  30259  esumpfinvallem  30264  esumpmono  30269  esummulc1  30271  esumcvg  30276  esumgect  30280  ofcval  30289  omssubadd  30490  sitgfval  30531  sitmcl  30541  sseqfv2  30584  cndprobval  30623  ballotlemfval  30679  ballotlemsv  30699  ballotlemsf1o  30703  ofcccat  30748  signsplypnf  30755  signsply0  30756  signstfval  30769  signshf  30793  reprpmtf1o  30832  reprdifc  30833  logdivsqrle  30856  hgt750lemg  30860  hgt750lema  30863  cvmliftlem8  31400  cvmliftphtlem  31425  mrsubval  31532  fwddifval  32394  knoppcnlem1  32608  knoppcnlem6  32613  unbdqndv2lem2  32626  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem19  33558  poimirlem22  33561  poimirlem23  33562  broucube  33573  dvtan  33590  itg2addnc  33594  ibladdnc  33597  itgaddnc  33600  itgmulc2nclem2  33607  itgmulc2nc  33608  itgabsnc  33609  ftc1cnnclem  33613  ftc1anclem3  33617  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  dvasin  33626  dvacos  33627  dvreasin  33628  dvreacos  33629  areacirclem1  33630  areacirc  33635  fsumshftd  34556  hlrelat5N  35005  mzpclall  37607  mzpsubst  37628  eldioph2  37642  rabdiophlem2  37683  irrapxlem1  37703  mzpcong  37856  mendlmod  38080  relexpmulnn  38318  iunrelexpuztr  38328  radcnvrat  38830  hashnzfzclim  38838  lhe4.4ex1a  38845  expgrowthi  38849  expgrowth  38851  bccval  38854  binomcxplemrat  38866  binomcxplemfrat  38867  binomcxplemradcnv  38868  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  mapsnend  39705  unirnmap  39714  unirnmapsn  39720  ssmapsn  39722  iocopn  40064  icoopn  40069  divcnvg  40177  sumnnodd  40180  climsubmpt  40210  dvsinax  40445  fperdvper  40451  dvdivf  40455  dvnprodlem1  40479  itgsincmulx  40508  stoweidlem59  40594  etransclem4  40773  etransclem13  40782  etransclem25  40794  etransclem48  40817  rrxtopnfi  40824  sge0tsms  40915  elhoi  41077  ovnval2  41080  ovnval2b  41087  ovncvrrp  41099  ovn0lem  41100  ovncl  41102  ovnome  41108  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvle  41135  ovnlecvr2  41145  ovncvr2  41146  ovnsubadd2lem  41180  ovnovollem1  41191  vonvolmbl  41196  iunhoiioolem  41210  vonioolem1  41215  vonioolem2  41216  vonicclem2  41219  smfresal  41316  smfres  41318  smfmullem4  41322  smfco  41330  pfxval  41708  fmtno  41766  intopval  42163  clintopval  42165  rngcval  42287  rnghmsscmap2  42298  rnghmsscmap  42299  rngchomALTV  42310  funcrngcsetc  42323  ringcval  42333  rhmsscmap2  42344  rhmsscmap  42345  funcringcsetc  42360  funcringcsetcALTV2lem5  42365  ringchomALTV  42373  funcringcsetclem5ALTV  42388  srhmsubclem3  42400  srhmsubc  42401  fldhmsubc  42409  srhmsubcALTVlem2  42418  srhmsubcALTV  42419  fldhmsubcALTV  42427  zlmodzxzscm  42460  zlmodzxzadd  42461  rmsupp0  42474  domnmsuppn0  42475  rmsuppss  42476  ply1mulgsumlem3  42501  ply1mulgsumlem4  42502  ply1mulgsum  42503  dmatALTval  42514  lincop  42522  lincval  42523  linc1  42539  lincresunit3lem1  42593  fdivmpt  42659  fdivmptfv  42664  refdivmptfv  42665  digval  42717
  Copyright terms: Public domain W3C validator