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

Theorem ovexd 7180
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 7178 . 2 (𝐴𝐹𝐵) ∈ V
21a1i 11 1 (𝜑 → (𝐴𝐹𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3492  (class class class)co 7145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-sn 4558  df-pr 4560  df-uni 4831  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  caofass  7432  caofdi  7434  caofdir  7435  caonncan  7436  suppofssd  7856  mapsnend  8576  snmapen  8578  pw2eng  8611  mapen  8669  mapxpen  8671  mapdom2  8676  cantnfcl  9118  cantnfle  9122  cantnflt  9123  cantnflt2  9124  cantnfp1lem2  9130  cantnfp1lem3  9131  cantnflem1b  9137  cantnflem1d  9139  cantnflem1  9140  cnfcomlem  9150  cnfcom  9151  cnfcom2lem  9152  cnfcom3lem  9154  fzen  12912  seqf1o  13399  wrdexg  13859  wrdnval  13884  pfxval  14023  pfxswrd  14056  splval  14101  cshwsexa  14174  ofccat  14317  climshftlem  14919  climshft  14921  climshft2  14927  caucvgr  15020  fsumrev  15122  hashdvds  16100  setsabs  16514  ressress  16550  firest  16694  prdsvscafval  16741  qusval  16803  xpsbas  16833  xpsadd  16835  xpsmul  16836  xpssca  16837  xpsvsca  16838  xpsless  16839  xpsle  16840  homfval  16950  comfval  16958  cicfval  17055  rescabs  17091  rescabs2  17092  resscat  17110  funcres2c  17159  ressffth  17196  fucbas  17218  fuccoval  17221  setchom  17328  catchom  17347  catcco  17349  estrchom  17365  funcestrcsetclem5  17382  funcsetcestrclem5  17397  evlf2val  17457  curf11  17464  curf12  17465  curf2val  17468  uncfval  17472  diagval  17478  hof2  17495  yonval  17499  gsumval2a  17883  gsumval2  17884  gsumwspan  17999  orbstafun  18379  orbstaval  18380  psgnvalii  18566  lsmhash  18760  frgpupval  18829  qusabl  18914  gsumval3  18956  gsumreidx  18966  gsumzaddlem  18970  gsummptshft  18985  telgsumfzslem  19037  telgsumfz  19039  telgsumfz0  19041  dpjval  19107  srgbinomlem3  19221  srgbinomlem4  19222  mulgass3  19316  lcomfsupp  19603  rmodislmodlem  19630  rmodislmod  19631  sraval  19877  srasca  19882  crngridl  19939  quscrng  19941  gsumbagdiaglem  20083  psrass1lem  20085  psrass1  20113  psrdi  20114  psrdir  20115  psrass23l  20116  mplval  20136  mplsubglem  20142  mplsubrglem  20147  mplmonmul  20173  mplcoe1  20174  opsrval  20183  psrbagev1  20218  evlslem6  20222  evlslem1  20223  evlsval  20227  mpfconst  20242  mpff  20245  mpfaddcl  20246  mpfmulcl  20247  mpfind  20248  mhpaddcl  20266  mhpinvcl  20267  mhpvscacl  20269  ply1lss  20292  gsumply1subr  20330  coe1add  20360  coe1tm  20369  coe1tmmul  20373  cply1mul  20390  ply1coe  20392  evl1expd  20436  pf1mpf  20443  pf1ind  20446  znval  20610  znzrhfo  20622  znunithash  20639  cygznlem2  20643  pjfval  20778  pjpm  20780  frlmgsum  20844  frlmipval  20851  frlmphllem  20852  frlmphl  20853  frlmsslsp  20868  frlmup1  20870  mamufv  20926  mamuass  20939  mamuvs1  20942  mamuvs2  20943  matgsum  20974  dmatmul  21034  scmatval  21041  scmatrhmval  21064  mvmulfv  21081  mavmulfv  21083  mavmulass  21086  marrepeval  21100  marepveval  21105  submaeval  21119  mdetrsca  21140  mdetunilem9  21157  mdetuni0  21158  gsummatr01lem3  21194  gsummatr01lem4  21195  gsummatr01  21196  smadiadetlem3  21205  cramerlem1  21224  mat2pmatmul  21267  m2cpminvid  21289  decpmatfsupp  21305  decpmatmullem  21307  decpmatmul  21308  decpmatmulsumfsupp  21309  pmatcollpw1lem1  21310  pmatcollpw3fi1lem1  21322  pmatcollpwscmatlem2  21326  pm2mpfval  21332  pm2mpf  21334  mply1topmatcllem  21339  mp2pm2mplem3  21344  mp2pm2mplem4  21345  pm2mpmhmlem1  21354  pm2mpmhmlem2  21355  pm2mp  21361  chfacfscmulfsupp  21395  chfacfscmulgsum  21396  chfacfpmmulfsupp  21399  chfacfpmmulgsum  21400  cpmidpmatlem3  21408  cpmadugsumlemB  21410  cpmadugsumlemC  21411  cpmadugsumlemF  21412  cayhamlem4  21424  xpstopnlem2  22347  fcfval  22569  tsmsxplem1  22688  tsmsxplem2  22689  tusval  22802  xpsdsfn  22914  xpsxmet  22917  xpsdsval  22918  xpsmet  22919  tmsval  23018  met1stc  23058  metuval  23086  cnmpopc  23459  pi1val  23568  pi1addf  23578  pi1addval  23579  pi1grplem  23580  rrxnm  23921  rrxcph  23922  rrxmval  23935  mbfmulc2  24191  mbfmul  24254  itg2mulclem  24274  ibladd  24348  itgadd  24352  itgabs  24362  bddmulibl  24366  dvmulf  24467  dvcmulf  24469  dvmptmul  24485  dvlip  24517  ftc1lem4  24563  mdegmullem  24599  coe1mul3  24620  r1pval  24677  plyco  24758  dgrcolem1  24790  elqaalem3  24837  taylpfval  24880  taylthlem2  24889  pserdvlem2  24943  advlogexp  25165  logtayl  25170  logccv  25173  dvcxp1  25248  dvcncxp1  25251  logbmpt  25293  logbfval  25295  relogbf  25296  dvatan  25440  cxp2lim  25481  cxploglim2  25483  lgamgulmlem2  25534  lgamgulm2  25540  lgamcvglem  25544  lgamf  25546  basellem7  25591  basellem8  25592  basellem9  25593  fsumdvdscom  25689  logexprlim  25728  dchrfi  25758  gausslemma2dlem2  25870  gausslemma2dlem3  25871  2lgslem1b  25895  chtppilimlem2  25977  chebbnd2  25980  chto1lb  25981  chpchtlim  25982  chpo1ub  25983  vmadivsum  25985  dchrisum0lem3  26022  mudivsum  26033  logdivsum  26036  log2sumbnd  26047  selberglem1  26048  selberg2lem  26053  selberg2  26054  selbergr  26071  wlkp1  27390  wwlksnextsurj  27605  wwlksnextbij  27607  clwlkclwwlklem2a1  27697  clwlkclwwlkf1  27715  eupth2eucrct  27923  frgrncvvdeq  28015  numclwlk2lem2fv  28084  numclwwlk2lem3  28086  ofoprabco  30337  fsuppcurry1  30387  fsuppcurry2  30388  offinsupp1  30389  ressprs  30569  resspos  30573  lmodvslmhm  30615  cycpmco2f1  30693  cycpmco2rn  30694  cycpmco2lem2  30696  cycpmco2lem3  30697  cycpmco2lem4  30698  cycpmco2lem5  30699  cycpmco2lem6  30700  cycpmco2  30702  archirngz  30745  archiabllem2a  30750  quslmod  30850  quslmhm  30851  qustriv  30856  qustrivr  30857  qsidomlem1  30882  qsidomlem2  30883  qusdimsum  30923  fedgmullem1  30924  fedgmullem2  30925  fedgmul  30926  submateq  30973  lmatcl  30980  mdetpmtr1  30987  madjusmdetlem1  30991  madjusmdetlem3  30993  qqhvval  31123  esumfzf  31227  esumpfinvallem  31232  esumpmono  31237  esummulc1  31239  esumcvg  31244  esumgect  31248  ofcval  31257  omssubadd  31457  sitgfval  31498  sitmcl  31508  sseqfv2  31551  cndprobval  31590  ballotlemfval  31646  ballotlemsv  31666  ballotlemsf1o  31670  ofcccat  31712  signsplypnf  31719  signsply0  31720  signstfval  31733  signshf  31757  reprpmtf1o  31796  reprdifc  31797  logdivsqrle  31820  hgt750lemg  31824  hgt750lema  31827  lpadval  31846  cvmliftlem8  32436  cvmliftphtlem  32461  fmla1  32531  gonarlem  32538  sategoelfvb  32563  mrsubval  32653  fwddifval  33520  knoppcnlem1  33729  knoppcnlem6  33734  unbdqndv2lem2  33746  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem5  34778  poimirlem6  34779  poimirlem7  34780  poimirlem10  34783  poimirlem11  34784  poimirlem12  34785  poimirlem16  34789  poimirlem19  34792  poimirlem22  34795  poimirlem23  34796  broucube  34807  dvtan  34823  itg2addnc  34827  ibladdnc  34830  itgaddnc  34833  itgmulc2nclem2  34840  itgmulc2nc  34841  itgabsnc  34842  ftc1cnnclem  34846  ftc1anclem3  34850  ftc1anclem6  34853  ftc1anclem7  34854  ftc1anclem8  34855  dvasin  34859  dvacos  34860  dvreasin  34861  dvreacos  34862  areacirclem1  34863  areacirc  34868  fsumshftd  35968  hlrelat5N  36417  selvcl  39016  frlmfzolen  39020  frlmfzoccat  39022  frlmvscadiccat  39023  prjspnval2  39145  0prjspnrel  39147  mzpclall  39202  mzpsubst  39223  eldioph2  39237  rabdiophlem2  39277  irrapxlem1  39297  mzpcong  39447  mendlmod  39671  relexpmulnn  39932  iunrelexpuztr  39942  radcnvrat  40523  hashnzfzclim  40531  lhe4.4ex1a  40538  expgrowthi  40542  expgrowth  40544  bccval  40547  binomcxplemrat  40559  binomcxplemfrat  40560  binomcxplemradcnv  40561  binomcxplemdvbinom  40562  binomcxplemdvsum  40564  binomcxplemnotnn0  40565  unirnmap  41347  unirnmapsn  41353  ssmapsn  41355  iocopn  41672  icoopn  41677  divcnvg  41784  sumnnodd  41787  climsubmpt  41817  dvsinax  42073  fperdvper  42079  dvdivf  42083  dvnprodlem1  42107  itgsincmulx  42135  stoweidlem59  42221  etransclem4  42400  etransclem13  42409  etransclem25  42421  etransclem48  42444  rrxtopnfi  42449  sge0tsms  42539  elhoi  42701  ovnval2  42704  ovnval2b  42711  ovncvrrp  42723  ovn0lem  42724  ovncl  42726  ovnome  42732  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvle  42759  ovnlecvr2  42769  ovncvr2  42770  ovnsubadd2lem  42804  ovnovollem1  42815  vonvolmbl  42820  iunhoiioolem  42834  vonioolem1  42839  vonioolem2  42840  vonicclem2  42843  smfresal  42940  smfres  42942  smfmullem4  42946  smfco  42954  fmtno  43568  efmnd  43969  intopval  44037  clintopval  44039  rngcval  44161  rnghmsscmap2  44172  rnghmsscmap  44173  rngchomALTV  44184  funcrngcsetc  44197  ringcval  44207  rhmsscmap2  44218  rhmsscmap  44219  funcringcsetc  44234  funcringcsetcALTV2lem5  44239  ringchomALTV  44247  funcringcsetclem5ALTV  44262  srhmsubclem3  44274  srhmsubc  44275  fldhmsubc  44283  srhmsubcALTVlem2  44292  srhmsubcALTV  44293  fldhmsubcALTV  44301  zlmodzxzscm  44333  zlmodzxzadd  44334  rmsupp0  44344  domnmsuppn0  44345  rmsuppss  44346  ply1mulgsumlem3  44370  ply1mulgsumlem4  44371  ply1mulgsum  44372  dmatALTval  44383  lincop  44391  lincval  44392  linc1  44408  lincresunit3lem1  44462  fdivmpt  44528  fdivmptfv  44533  refdivmptfv  44534  digval  44586  line2xlem  44668
  Copyright terms: Public domain W3C validator