Theorem inidm 4178

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 4163	1 ⊢ (𝐴 ∩ 𝐴) = 𝐴

Syntax hints:   = wceq 1540   ∈ wcel 2109   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910

This theorem is referenced by:  inindi  4186  inindir  4187  uneqin  4240  disjeq0  4407  ssdifeq0  4438  intsng  4933  xpindi  5776  xpindir  5777  resindm  5981  elidinxpid  5996  idinxpresid  5999  predidm  6274  offval2f  7628  fnfvof  7630  ofres  7632  offval2  7633  ofrfval2  7634  coof  7637  ofco  7638  offveq  7639  offveqb  7640  ofc1  7641  ofc2  7642  caofref  7644  caofrss  7652  caoftrn  7654  offsplitfpar  8052  suppssof1  8132  suppofssd  8136  suppofss1d  8137  suppofss2d  8138  fisn  9317  dffi3  9321  ofsubeq0  12125  ofnegsub  12126  ofsubge0  12127  seqof  13966  ofccat  14876  incexc  15744  sadeq  16383  smuval2  16393  smumul  16404  ressinbas  17156  pwsle  17396  pwsleval  17397  mndpsuppss  18639  mndvcl  18671  ghmplusg  19725  gsumzaddlem  19800  gsumzadd  19801  gsumle  20024  pwspjmhmmgpd  20213  lcomf  20804  crng2idl  21188  frlmipval  21686  frlmphllem  21687  frlmphl  21688  frlmsslsp  21703  frlmup1  21705  psrbaglesupp  21829  psrbagaddcl  21831  psrbagcon  21832  psrbaglefi  21833  psrbagleadd1  21835  psrbagconf1o  21836  gsumbagdiaglem  21837  psraddcl  21845  psraddclOLD  21846  psrvscacl  21858  psrlidm  21869  psrdi  21872  psrdir  21873  psrascl  21886  mplsubglem  21906  psrbagev1  21982  evlslem3  21985  evlslem1  21987  mhpmulcl  22034  psdmplcl  22047  psdadd  22048  psdmul  22051  psdmvr  22054  psrplusgpropd  22118  coe1add  22148  pf1ind  22240  evls1fpws  22254  matplusgcell  22318  matsubgcell  22319  mat1dimscm  22360  baspartn  22839  indistopon  22886  epttop  22894  dissnlocfin  23414  ptbasin  23462  snfil  23749  tsmsadd  24032  ust0  24105  ustuqtop1  24127  rrxcph  25290  rrxds  25291  volun  25444  mbfmulc2lem  25546  mbfaddlem  25559  0pledm  25572  i1faddlem  25592  i1fmullem  25593  i1fadd  25594  i1fmul  25595  itg1addlem4  25598  i1fmulclem  25601  i1fmulc  25602  itg1lea  25611  itg1le  25612  mbfi1fseqlem5  25618  mbfi1flimlem  25621  mbfmullem2  25623  xrge0f  25630  itg2ge0  25634  itg2lea  25643  itg2mulclem  25645  itg2mulc  25646  itg2splitlem  25647  itg2split  25648  itg2monolem1  25649  itg2mono  25652  itg2i1fseqle  25653  itg2i1fseq  25654  itg2addlem  25657  itg2cnlem1  25660  dvaddf  25843  dvmulf  25844  dvcmulf  25846  dv11cn  25904  plyaddlem1  26116  plyaddlem  26118  coeeulem  26127  coeaddlem  26152  coemulc  26158  dgradd2  26172  dgrcolem2  26178  ofmulrt  26187  plydivlem3  26201  plydivlem4  26202  plydiveu  26204  plyrem  26211  vieta1lem2  26217  elqaalem3  26227  qaa  26229  jensenlem2  26896  jensen  26897  basellem7  26995  basellem9  26997  dchrmulcl  27158  chssoc  31440  chjidm  31464  mdslmd3i  32276  inin  32460  unidifsnne  32480  disjnf  32514  ofrn  32583  ofrn2  32584  ofresid  32586  offinsupp1  32671  tocyccntz  33087  elrgspnlem1  33183  islinds5  33305  ellspds  33306  1arithidomlem2  33474  1arithidom  33475  ply1gsumz  33532  ply1degltdimlem  33595  fedgmullem1  33602  extdgfialglem2  33666  hauseqcn  33871  ofcof  34080  carsgclctunlem1  34291  carsgclctun  34295  sibfof  34314  plymul02  34520  signshf  34562  circlemethhgt  34617  msrid  35528  nepss  35701  bj-inrab2  36912  matunitlindflem1  37606  matunitlindflem2  37607  poimirlem1  37611  poimirlem2  37612  poimirlem3  37613  poimirlem4  37614  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem10  37620  poimirlem11  37621  poimirlem12  37622  poimirlem16  37626  poimirlem17  37627  poimirlem19  37629  poimirlem20  37630  poimirlem23  37633  poimirlem24  37634  poimirlem25  37635  poimirlem28  37638  poimirlem29  37639  poimirlem30  37640  poimirlem31  37641  poimirlem32  37642  broucube  37644  itg2addnclem  37661  itg2addnclem3  37663  itg2addnc  37664  ftc1anclem3  37685  ftc1anclem5  37687  ftc1anclem6  37688  ftc1anclem8  37690  blbnd  37777  lshpinN  38978  lfladdcl  39060  lflvscl  39066  ldualvaddval  39120  lclkrlem2e  41500  ofun  42219  mplmapghm  42539  evlsvvval  42546  fsuppind  42573  fsuppssind  42576  mhphf  42580  mzpclall  42710  mzpindd  42729  dgrsub2  43118  mpaaeu  43133  mendring  43171  ofoafo  43339  ofoacl  43340  ofoaid1  43341  ofoaid2  43342  ofoaass  43343  ofoacom  43344  naddcnff  43345  naddcnffo  43347  naddcnfcom  43349  naddcnfid1  43350  naddcnfass  43352  relexpaddss  43701  ntrkbimka  44021  clsk3nimkb  44023  caofcan  44306  ofmul12  44308  ofdivrec  44309  ofdivcan4  44310  ofdivdiv2  44311  expgrowth  44318  binomcxplemrat  44333  binomcxplemnotnn0  44339  disjf1  45171  dvsinax  45904  dvcosax  45917  dvdivcncf  45918  meadjun  46453  smfmulc1  46787  cjnpoly  46883  f1cof1blem  47068  isubgr0uhgr  47867  uzlidlring  48229  ofaddmndmap  48337  dmatALTbas  48396  dflinc2  48405  fdivmpt  48535  zeroopropdlem  49237  incat  49596  aacllem  49796  amgmwlem  49797