Theorem inidm 4149

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.

Step	Hyp	Ref	Expression
1		anidm 564	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	ineqri 4135	1 ⊢ (𝐴 ∩ 𝐴) = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2108   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  inindi  4157  inindir  4158  uneqin  4209  disjeq0  4386  ssdifeq0  4414  intsng  4913  xpindi  5731  xpindir  5732  resindm  5929  elidinxpid  5941  idinxpresid  5944  predidm  6218  offval2f  7526  fnfvof  7528  ofres  7530  offval2  7531  ofrfval2  7532  ofco  7534  offveq  7535  offveqb  7536  ofc1  7537  ofc2  7538  caofref  7540  caofrss  7547  caoftrn  7549  offsplitfpar  7931  suppssof1  7986  suppofssd  7990  suppofss1d  7991  suppofss2d  7992  fisn  9116  dffi3  9120  ofsubeq0  11900  ofnegsub  11901  ofsubge0  11902  seqof  13708  ofccat  14608  incexc  15477  sadeq  16107  smuval2  16117  smumul  16128  ressinbas  16881  pwsle  17120  pwsleval  17121  ghmplusg  19362  gsumzaddlem  19437  gsumzadd  19438  lcomf  20077  crng2idl  20423  frlmipval  20896  frlmphllem  20897  frlmphl  20898  frlmsslsp  20913  frlmup1  20915  psrbaglesupp  21037  psrbaglesuppOLD  21038  psrbagaddcl  21041  psrbagaddclOLD  21042  psrbagcon  21043  psrbagconOLD  21044  psrbaglefi  21045  psrbaglefiOLD  21046  psrbagconf1o  21049  psrbagconf1oOLD  21050  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  psraddcl  21062  psrvscacl  21072  psrlidm  21082  psrdi  21085  psrdir  21086  mplsubglem  21115  psrbagev1  21195  psrbagev1OLD  21196  evlslem3  21200  evlslem1  21202  mhpmulcl  21249  psrplusgpropd  21317  coe1add  21345  pf1ind  21431  mndvcl  21450  matplusgcell  21490  matsubgcell  21491  mat1dimscm  21532  baspartn  22012  indistopon  22059  epttop  22067  dissnlocfin  22588  ptbasin  22636  snfil  22923  tsmsadd  23206  ust0  23279  ustuqtop1  23301  rrxcph  24461  rrxds  24462  volun  24614  mbfmulc2lem  24716  mbfaddlem  24729  0pledm  24742  i1faddlem  24762  i1fmullem  24763  i1fadd  24764  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  i1fmulclem  24772  i1fmulc  24773  itg1lea  24782  itg1le  24783  mbfi1fseqlem5  24789  mbfi1flimlem  24792  mbfmullem2  24794  xrge0f  24801  itg2ge0  24805  itg2lea  24814  itg2mulclem  24816  itg2mulc  24817  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itg2mono  24823  itg2i1fseqle  24824  itg2i1fseq  24825  itg2addlem  24828  itg2cnlem1  24831  dvaddf  25011  dvmulf  25012  dvcmulf  25014  dv11cn  25070  plyaddlem1  25279  plyaddlem  25281  coeeulem  25290  coeaddlem  25315  coemulc  25321  dgradd2  25334  dgrcolem2  25340  ofmulrt  25347  plydivlem3  25360  plydivlem4  25361  plydiveu  25363  plyrem  25370  vieta1lem2  25376  elqaalem3  25386  qaa  25388  jensenlem2  26042  jensen  26043  basellem7  26141  basellem9  26143  dchrmulcl  26302  chssoc  29759  chjidm  29783  mdslmd3i  30595  inin  30763  unidifsnne  30785  disjnf  30810  ofrn  30877  ofrn2  30878  ofresid  30880  offinsupp1  30964  gsumle  31252  tocyccntz  31313  islinds5  31465  ellspds  31466  fedgmullem1  31612  hauseqcn  31750  ofcof  31975  carsgclctunlem1  32184  carsgclctun  32188  sibfof  32207  plymul02  32425  signshf  32467  circlemethhgt  32523  msrid  33407  nepss  33564  bj-inrab2  35043  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  broucube  35738  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  ftc1anclem3  35779  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem8  35784  blbnd  35872  lshpinN  36930  lfladdcl  37012  lflvscl  37018  ldualvaddval  37072  lclkrlem2e  39452  ofun  40137  pwspjmhmmgpd  40192  evlsbagval  40198  fsuppind  40202  fsuppssind  40205  mhphf  40208  mzpclall  40465  mzpindd  40484  dgrsub2  40876  mpaaeu  40891  mendring  40933  relexpaddss  41215  ntrkbimka  41537  clsk3nimkb  41539  caofcan  41830  ofmul12  41832  ofdivrec  41833  ofdivcan4  41834  ofdivdiv2  41835  expgrowth  41842  binomcxplemrat  41857  binomcxplemnotnn0  41863  disjf1  42609  dvsinax  43344  dvcosax  43357  dvdivcncf  43358  meadjun  43890  smfmulc1  44217  f1cof1blem  44455  uzlidlring  45375  ofaddmndmap  45567  mndpsuppss  45595  dmatALTbas  45630  dflinc2  45639  fdivmpt  45774  aacllem  46391  amgmwlem  46392