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

Theorem inidm 4180
Description: Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
inidm (𝐴𝐴) = 𝐴

Proof of Theorem inidm
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 anidm 568 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21ineqri 4165 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  cin 3918
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-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926
This theorem is referenced by:  inindi  4188  inindir  4189  uneqin  4240  disjeq0  4388  ssdifeq0  4415  intsng  4897  xpindi  5691  xpindir  5692  resindm  5887  elidinxpid  5899  idinxpresid  5902  predidm  6157  offval2f  7415  fnfvof  7417  ofres  7419  offval2  7420  ofrfval2  7421  ofco  7423  offveq  7424  offveqb  7425  ofc1  7426  ofc2  7427  caofref  7429  caofrss  7436  caoftrn  7438  offsplitfpar  7811  suppssof1  7859  suppofssd  7863  suppofss1d  7864  suppofss2d  7865  fisn  8888  dffi3  8892  ofsubeq0  11631  ofnegsub  11632  ofsubge0  11633  seqof  13432  ofccat  14329  incexc  15192  sadeq  15819  smuval2  15829  smumul  15840  ressinbas  16560  pwsle  16765  pwsleval  16766  ghmplusg  18966  gsumzaddlem  19041  gsumzadd  19042  lcomf  19673  lcomfsupp  19674  crng2idl  20012  psrbaglesupp  20148  psrbagaddcl  20150  psrbagcon  20151  psrbaglefi  20152  psrbagconf1o  20154  gsumbagdiaglem  20155  psraddcl  20163  psrvscacl  20173  psrlidm  20183  psrdi  20186  psrdir  20187  mplsubglem  20214  psrbagev1  20290  evlslem3  20293  evlslem1  20295  psrplusgpropd  20404  coe1add  20432  pf1ind  20518  frlmipval  20923  frlmphllem  20924  frlmphl  20925  frlmsslsp  20940  frlmup1  20942  mndvcl  21002  matplusgcell  21042  matsubgcell  21043  mat1dimscm  21084  baspartn  21562  indistopon  21609  epttop  21617  dissnlocfin  22137  ptbasin  22185  snfil  22472  tsmsadd  22755  ust0  22828  ustuqtop1  22850  rrxcph  23999  rrxds  24000  volun  24152  mbfmulc2lem  24254  mbfaddlem  24267  0pledm  24280  i1faddlem  24300  i1fmullem  24301  i1fadd  24302  i1fmul  24303  itg1addlem4  24306  i1fmulclem  24309  i1fmulc  24310  itg1lea  24319  itg1le  24320  mbfi1fseqlem5  24326  mbfi1flimlem  24329  mbfmullem2  24331  xrge0f  24338  itg2ge0  24342  itg2lea  24351  itg2mulclem  24353  itg2mulc  24354  itg2splitlem  24355  itg2split  24356  itg2monolem1  24357  itg2mono  24360  itg2i1fseqle  24361  itg2i1fseq  24362  itg2addlem  24365  itg2cnlem1  24368  dvaddf  24548  dvmulf  24549  dvcmulf  24551  dv11cn  24607  plyaddlem1  24813  plyaddlem  24815  coeeulem  24824  coeaddlem  24849  coemulc  24855  dgradd2  24868  dgrcolem2  24874  ofmulrt  24881  plydivlem3  24894  plydivlem4  24895  plydiveu  24897  plyrem  24904  vieta1lem2  24910  elqaalem3  24920  qaa  24922  jensenlem2  25576  jensen  25577  basellem7  25675  basellem9  25677  dchrmulcl  25836  chssoc  29282  chjidm  29306  mdslmd3i  30118  inin  30288  unidifsnne  30307  disjnf  30331  ofrn  30397  ofrn2  30398  ofresid  30400  offinsupp1  30474  gsumle  30757  tocyccntz  30818  islinds5  30965  ellspds  30966  fedgmullem1  31085  hauseqcn  31198  ofcof  31423  carsgclctunlem1  31632  carsgclctun  31636  sibfof  31655  plymul02  31873  signshf  31915  circlemethhgt  31971  msrid  32849  nepss  33005  bj-inrab2  34314  matunitlindflem1  34998  matunitlindflem2  34999  poimirlem1  35003  poimirlem2  35004  poimirlem3  35005  poimirlem4  35006  poimirlem6  35008  poimirlem7  35009  poimirlem8  35010  poimirlem10  35012  poimirlem11  35013  poimirlem12  35014  poimirlem16  35018  poimirlem17  35019  poimirlem19  35021  poimirlem20  35022  poimirlem23  35025  poimirlem24  35026  poimirlem25  35027  poimirlem28  35030  poimirlem29  35031  poimirlem30  35032  poimirlem31  35033  poimirlem32  35034  broucube  35036  itg2addnclem  35053  itg2addnclem3  35055  itg2addnc  35056  ftc1anclem3  35077  ftc1anclem5  35079  ftc1anclem6  35080  ftc1anclem8  35082  blbnd  35170  lshpinN  36230  lfladdcl  36312  lflvscl  36318  ldualvaddval  36372  lclkrlem2e  38752  mzpclall  39584  mzpindd  39603  dgrsub2  39995  mpaaeu  40010  mendring  40052  relexpaddss  40335  ntrkbimka  40660  clsk3nimkb  40662  caofcan  40947  ofmul12  40949  ofdivrec  40950  ofdivcan4  40951  ofdivdiv2  40952  expgrowth  40959  binomcxplemrat  40974  binomcxplemnotnn0  40980  disjf1  41734  dvsinax  42481  dvcosax  42494  dvdivcncf  42495  meadjun  43027  smfmulc1  43354  uzlidlring  44479  ofaddmndmap  44671  mndpsuppss  44699  mndpfsupp  44704  dmatALTbas  44736  dflinc2  44745  fdivmpt  44880  aacllem  45255  amgmwlem  45256
  Copyright terms: Public domain W3C validator