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

Theorem ovexd 7165
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 7163 . 2 (𝐴𝐹𝐵) ∈ V
21a1i 11 1 (𝜑 → (𝐴𝐹𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  Vcvv 3471  (class class class)co 7130
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-nul 5183
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-sn 4541  df-pr 4543  df-uni 4812  df-iota 6287  df-fv 6336  df-ov 7133
This theorem is referenced by:  caofass  7418  caofdi  7420  caofdir  7421  caonncan  7422  suppofssd  7842  mapsnend  8563  snmapen  8565  pw2eng  8598  mapen  8657  mapxpen  8659  mapdom2  8664  cantnfcl  9106  cantnfle  9110  cantnflt  9111  cantnflt2  9112  cantnfp1lem2  9118  cantnfp1lem3  9119  cantnflem1b  9125  cantnflem1d  9127  cantnflem1  9128  cnfcomlem  9138  cnfcom  9139  cnfcom2lem  9140  cnfcom3lem  9142  fzen  12907  seqf1o  13395  wrdexg  13855  wrdnval  13876  pfxval  14014  pfxswrd  14047  splval  14092  cshwsexa  14165  ofccat  14308  climshftlem  14910  climshft  14912  climshft2  14918  caucvgr  15011  fsumrev  15113  hashdvds  16089  setsabs  16504  ressress  16540  firest  16684  prdsvscafval  16731  qusval  16793  xpsbas  16823  xpsadd  16825  xpsmul  16826  xpssca  16827  xpsvsca  16828  xpsless  16829  xpsle  16830  homfval  16940  comfval  16948  cicfval  17045  rescabs  17081  rescabs2  17082  resscat  17100  funcres2c  17149  ressffth  17186  fucbas  17208  fuccoval  17211  setchom  17318  catchom  17337  catcco  17339  estrchom  17355  funcestrcsetclem5  17372  funcsetcestrclem5  17387  evlf2val  17447  curf11  17454  curf12  17455  curf2val  17458  uncfval  17462  diagval  17468  hof2  17485  yonval  17489  gsumval2a  17873  gsumval2  17874  gsumwspan  17989  efmnd  18013  orbstafun  18419  orbstaval  18420  symgval  18475  psgnvalii  18615  lsmhash  18809  frgpupval  18878  qusabl  18963  gsumval3  19005  gsumreidx  19015  gsumzaddlem  19019  gsummptshft  19034  telgsumfzslem  19086  telgsumfz  19088  telgsumfz0  19090  dpjval  19156  srgbinomlem3  19270  srgbinomlem4  19271  mulgass3  19365  lcomfsupp  19649  rmodislmodlem  19676  rmodislmod  19677  sraval  19923  srasca  19928  crngridl  19986  quscrng  19988  gsumbagdiaglem  20130  psrass1lem  20132  psrass1  20160  psrdi  20161  psrdir  20162  psrass23l  20163  mplval  20183  mplsubglem  20189  mplsubrglem  20194  mplmonmul  20220  mplcoe1  20221  opsrval  20230  psrbagev1  20265  evlslem6  20269  evlslem1  20270  evlsval  20274  mpfconst  20289  mpff  20292  mpfaddcl  20293  mpfmulcl  20294  mpfind  20295  mhpaddcl  20313  mhpinvcl  20314  mhpvscacl  20316  ply1lss  20339  gsumply1subr  20377  coe1add  20407  coe1tm  20416  coe1tmmul  20420  cply1mul  20437  ply1coe  20439  evl1expd  20483  pf1mpf  20490  pf1ind  20493  znval  20657  znzrhfo  20669  znunithash  20686  cygznlem2  20690  pjfval  20825  pjpm  20827  frlmgsum  20891  frlmipval  20898  frlmphllem  20899  frlmphl  20900  frlmsslsp  20915  frlmup1  20917  mamufv  20973  mamuass  20986  mamuvs1  20989  mamuvs2  20990  matgsum  21021  dmatmul  21081  scmatval  21088  scmatrhmval  21111  mvmulfv  21128  mavmulfv  21130  mavmulass  21133  marrepeval  21147  marepveval  21152  submaeval  21166  mdetrsca  21187  mdetunilem9  21204  mdetuni0  21205  gsummatr01lem3  21241  gsummatr01lem4  21242  gsummatr01  21243  smadiadetlem3  21252  cramerlem1  21271  mat2pmatmul  21314  m2cpminvid  21336  decpmatfsupp  21352  decpmatmullem  21354  decpmatmul  21355  decpmatmulsumfsupp  21356  pmatcollpw1lem1  21357  pmatcollpw3fi1lem1  21369  pmatcollpwscmatlem2  21373  pm2mpfval  21379  pm2mpf  21381  mply1topmatcllem  21386  mp2pm2mplem3  21391  mp2pm2mplem4  21392  pm2mpmhmlem1  21401  pm2mpmhmlem2  21402  pm2mp  21408  chfacfscmulfsupp  21442  chfacfscmulgsum  21443  chfacfpmmulfsupp  21446  chfacfpmmulgsum  21447  cpmidpmatlem3  21455  cpmadugsumlemB  21457  cpmadugsumlemC  21458  cpmadugsumlemF  21459  cayhamlem4  21471  xpstopnlem2  22394  fcfval  22616  tsmsxplem1  22736  tsmsxplem2  22737  tusval  22850  xpsdsfn  22962  xpsxmet  22965  xpsdsval  22966  xpsmet  22967  tmsval  23066  met1stc  23106  metuval  23134  cnmpopc  23511  pi1val  23620  pi1addf  23630  pi1addval  23631  pi1grplem  23632  rrxnm  23973  rrxcph  23974  rrxmval  23987  mbfmulc2  24245  mbfmul  24308  itg2mulclem  24328  ibladd  24402  itgadd  24406  itgabs  24416  bddmulibl  24420  dvmulf  24524  dvcmulf  24526  dvmptmul  24542  dvlip  24574  ftc1lem4  24620  mdegmullem  24657  coe1mul3  24678  r1pval  24735  plyco  24816  dgrcolem1  24848  elqaalem3  24895  taylpfval  24938  taylthlem2  24947  pserdvlem2  25001  advlogexp  25224  logtayl  25229  logccv  25232  dvcxp1  25307  dvcncxp1  25310  logbmpt  25352  logbfval  25354  relogbf  25355  dvatan  25499  cxp2lim  25540  cxploglim2  25542  lgamgulmlem2  25593  lgamgulm2  25599  lgamcvglem  25603  lgamf  25605  basellem7  25650  basellem8  25651  basellem9  25652  fsumdvdscom  25748  logexprlim  25787  dchrfi  25817  gausslemma2dlem2  25929  gausslemma2dlem3  25930  2lgslem1b  25954  chtppilimlem2  26036  chebbnd2  26039  chto1lb  26040  chpchtlim  26041  chpo1ub  26042  vmadivsum  26044  dchrisum0lem3  26081  mudivsum  26092  logdivsum  26095  log2sumbnd  26106  selberglem1  26107  selberg2lem  26112  selberg2  26113  selbergr  26130  wlkp1  27449  wwlksnextsurj  27664  wwlksnextbij  27666  clwlkclwwlklem2a1  27755  clwlkclwwlkf1  27773  eupth2eucrct  27980  frgrncvvdeq  28072  numclwlk2lem2fv  28141  numclwwlk2lem3  28143  ofoprabco  30395  fsuppcurry1  30447  fsuppcurry2  30448  offinsupp1  30449  ressprs  30628  resspos  30632  mntoval  30650  mgcoval  30654  lmodvslmhm  30695  cycpmco2f1  30773  cycpmco2rn  30774  cycpmco2lem2  30776  cycpmco2lem3  30777  cycpmco2lem4  30778  cycpmco2lem5  30779  cycpmco2lem6  30780  cycpmco2  30782  archirngz  30825  archiabllem2a  30830  quslmod  30930  quslmhm  30931  qustriv  30936  qustrivr  30937  qsidomlem1  30975  qsidomlem2  30976  qusdimsum  31034  fedgmullem1  31035  fedgmullem2  31036  fedgmul  31037  submateq  31084  lmatcl  31091  mdetpmtr1  31098  madjusmdetlem1  31102  madjusmdetlem3  31104  qqhvval  31231  esumfzf  31335  esumpfinvallem  31340  esumpmono  31345  esummulc1  31347  esumcvg  31352  esumgect  31356  ofcval  31365  omssubadd  31565  sitgfval  31606  sitmcl  31616  sseqfv2  31659  cndprobval  31698  ballotlemfval  31754  ballotlemsv  31774  ballotlemsf1o  31778  ofcccat  31820  signsplypnf  31827  signsply0  31828  signstfval  31841  signshf  31865  reprpmtf1o  31904  reprdifc  31905  logdivsqrle  31928  hgt750lemg  31932  hgt750lema  31935  lpadval  31954  cvmliftlem8  32546  cvmliftphtlem  32571  fmla1  32641  gonarlem  32648  sategoelfvb  32673  mrsubval  32763  fwddifval  33630  knoppcnlem1  33839  knoppcnlem6  33844  unbdqndv2lem2  33856  poimirlem1  34938  poimirlem2  34939  poimirlem3  34940  poimirlem5  34942  poimirlem6  34943  poimirlem7  34944  poimirlem10  34947  poimirlem11  34948  poimirlem12  34949  poimirlem16  34953  poimirlem19  34956  poimirlem22  34959  poimirlem23  34960  broucube  34971  dvtan  34987  itg2addnc  34991  ibladdnc  34994  itgaddnc  34997  itgmulc2nclem2  35004  itgmulc2nc  35005  itgabsnc  35006  ftc1cnnclem  35008  ftc1anclem3  35012  ftc1anclem6  35015  ftc1anclem7  35016  ftc1anclem8  35017  dvasin  35021  dvacos  35022  dvreasin  35023  dvreacos  35024  areacirclem1  35025  areacirc  35030  fsumshftd  36128  hlrelat5N  36577  selvcl  39254  frlmfzolen  39258  frlmfzoccat  39260  frlmvscadiccat  39261  prjspnval2  39408  0prjspnrel  39410  mzpclall  39465  mzpsubst  39486  eldioph2  39500  rabdiophlem2  39540  irrapxlem1  39560  mzpcong  39710  mendlmod  39934  relexpmulnn  40191  iunrelexpuztr  40201  mnringvald  40706  mnringmulrvald  40720  radcnvrat  40803  hashnzfzclim  40811  lhe4.4ex1a  40818  expgrowthi  40822  expgrowth  40824  bccval  40827  binomcxplemrat  40839  binomcxplemfrat  40840  binomcxplemradcnv  40841  binomcxplemdvbinom  40842  binomcxplemdvsum  40844  binomcxplemnotnn0  40845  unirnmap  41627  unirnmapsn  41633  ssmapsn  41635  iocopn  41950  icoopn  41955  divcnvg  42062  sumnnodd  42065  climsubmpt  42095  dvsinax  42348  fperdvper  42354  dvdivf  42357  dvnprodlem1  42381  itgsincmulx  42409  stoweidlem59  42494  etransclem4  42673  etransclem13  42682  etransclem25  42694  etransclem48  42717  rrxtopnfi  42722  sge0tsms  42812  elhoi  42974  ovnval2  42977  ovnval2b  42984  ovncvrrp  42996  ovn0lem  42997  ovncl  42999  ovnome  43005  hoidmvlelem2  43028  hoidmvlelem3  43029  hoidmvle  43032  ovnlecvr2  43042  ovncvr2  43043  ovnsubadd2lem  43077  ovnovollem1  43088  vonvolmbl  43093  iunhoiioolem  43107  vonioolem1  43112  vonioolem2  43113  vonicclem2  43116  smfresal  43213  smfres  43215  smfmullem4  43219  smfco  43227  fmtno  43839  intopval  44256  clintopval  44258  rngcval  44380  rnghmsscmap2  44391  rnghmsscmap  44392  rngchomALTV  44403  funcrngcsetc  44416  ringcval  44426  rhmsscmap2  44437  rhmsscmap  44438  funcringcsetc  44453  funcringcsetcALTV2lem5  44458  ringchomALTV  44466  funcringcsetclem5ALTV  44481  srhmsubclem3  44493  srhmsubc  44494  fldhmsubc  44502  srhmsubcALTVlem2  44511  srhmsubcALTV  44512  fldhmsubcALTV  44520  zlmodzxzscm  44552  zlmodzxzadd  44553  rmsupp0  44563  domnmsuppn0  44564  rmsuppss  44565  ply1mulgsumlem3  44589  ply1mulgsumlem4  44590  ply1mulgsum  44591  dmatALTval  44602  lincop  44610  lincval  44611  linc1  44627  lincresunit3lem1  44681  fdivmpt  44747  fdivmptfv  44752  refdivmptfv  44753  digval  44805  itcovalpclem1  44846  itcovalt2lem1  44851  ackvalsuc1mpt  44854  ackval1  44857  ackval2  44858  ackval3  44859  ackval42  44872  line2xlem  44929
  Copyright terms: Public domain W3C validator