Theorem inidm 4167

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

Syntax hints:   = wceq 1542   ∈ wcel 2114   ∩ cin 3888

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  inindi  4175  inindir  4176  uneqin  4229  disjeq0  4396  ssdifeq0  4426  intsng  4925  xpindi  5788  xpindir  5789  resindm  5995  elidinxpid  6010  idinxpresid  6013  predidm  6290  offval2f  7646  fnfvof  7648  ofres  7650  offval2  7651  ofrfval2  7652  coof  7655  ofco  7656  offveq  7657  offveqb  7658  ofc1  7659  ofc2  7660  caofref  7662  caofrss  7670  caoftrn  7672  offsplitfpar  8069  suppssof1  8149  suppofssd  8153  suppofss1d  8154  suppofss2d  8155  fisn  9340  dffi3  9344  ofsubeq0  12156  ofnegsub  12157  ofsubge0  12158  seqof  14021  ofccat  14931  incexc  15802  sadeq  16441  smuval2  16451  smumul  16462  ressinbas  17215  pwsle  17456  pwsleval  17457  mndpsuppss  18733  mndvcl  18765  ghmplusg  19821  gsumzaddlem  19896  gsumzadd  19897  gsumle  20120  pwspjmhmmgpd  20307  lcomf  20896  crng2idl  21279  frlmipval  21759  frlmphllem  21760  frlmphl  21761  frlmsslsp  21776  frlmup1  21778  psrbaglesupp  21902  psrbagaddcl  21904  psrbagcon  21905  psrbaglefi  21906  psrbagleadd1  21908  psrbagconf1o  21909  gsumbagdiaglem  21910  psraddcl  21918  psrvscacl  21930  psrlidm  21940  psrdi  21943  psrdir  21944  psrascl  21957  mplsubglem  21977  psrbagev1  22055  evlslem3  22058  evlslem1  22060  evlsvvval  22071  mhpmulcl  22115  psdmplcl  22128  psdadd  22129  psdmul  22132  psdmvr  22135  psrplusgpropd  22199  coe1add  22229  pf1ind  22320  evls1fpws  22334  matplusgcell  22398  matsubgcell  22399  mat1dimscm  22440  baspartn  22919  indistopon  22966  epttop  22974  dissnlocfin  23494  ptbasin  23542  snfil  23829  tsmsadd  24112  ust0  24185  ustuqtop1  24206  rrxcph  25359  rrxds  25360  volun  25512  mbfmulc2lem  25614  mbfaddlem  25627  0pledm  25640  i1faddlem  25660  i1fmullem  25661  i1fadd  25662  i1fmul  25663  itg1addlem4  25666  i1fmulclem  25669  i1fmulc  25670  itg1lea  25679  itg1le  25680  mbfi1fseqlem5  25686  mbfi1flimlem  25689  mbfmullem2  25691  xrge0f  25698  itg2ge0  25702  itg2lea  25711  itg2mulclem  25713  itg2mulc  25714  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2mono  25720  itg2i1fseqle  25721  itg2i1fseq  25722  itg2addlem  25725  itg2cnlem1  25728  dvaddf  25909  dvmulf  25910  dvcmulf  25912  dv11cn  25968  plyaddlem1  26178  plyaddlem  26180  coeeulem  26189  coeaddlem  26214  coemulc  26220  dgradd2  26233  dgrcolem2  26239  ofmulrt  26248  plydivlem3  26261  plydivlem4  26262  plydiveu  26264  plyrem  26271  vieta1lem2  26277  elqaalem3  26287  qaa  26289  jensenlem2  26951  jensen  26952  basellem7  27050  basellem9  27052  dchrmulcl  27212  chssoc  31567  chjidm  31591  mdslmd3i  32403  inin  32586  unidifsnne  32606  disjnf  32640  fnfvor  32682  ofrco  32683  ofrn  32712  ofrn2  32713  ofresid  32715  offinsupp1  32799  tocyccntz  33205  elrgspnlem1  33303  islinds5  33427  ellspds  33428  1arithidomlem2  33596  1arithidom  33597  ply1gsumz  33659  mplvrpmrhm  33691  esplyind  33719  ply1degltdimlem  33766  fedgmullem1  33773  extdgfialglem2  33837  hauseqcn  34042  ofcof  34251  carsgclctunlem1  34461  carsgclctun  34465  sibfof  34484  plymul02  34690  signshf  34732  circlemethhgt  34787  msrid  35727  nepss  35900  bj-inrab2  37235  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  broucube  37975  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  ftc1anclem3  38016  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem8  38021  blbnd  38108  disjimeceqim  39125  lshpinN  39435  lfladdcl  39517  lflvscl  39523  ldualvaddval  39577  lclkrlem2e  41957  ofun  42677  mplmapghm  42997  fsuppind  43023  fsuppssind  43026  mhphf  43030  mzpclall  43159  mzpindd  43178  dgrsub2  43563  mpaaeu  43578  mendring  43616  ofoafo  43784  ofoacl  43785  ofoaid1  43786  ofoaid2  43787  ofoaass  43788  ofoacom  43789  naddcnff  43790  naddcnffo  43792  naddcnfcom  43794  naddcnfid1  43795  naddcnfass  43797  relexpaddss  44145  ntrkbimka  44465  clsk3nimkb  44467  caofcan  44750  ofmul12  44752  ofdivrec  44753  ofdivcan4  44754  ofdivdiv2  44755  expgrowth  44762  binomcxplemrat  44777  binomcxplemnotnn0  44783  disjf1  45613  dvsinax  46341  dvcosax  46354  dvdivcncf  46355  meadjun  46890  smfmulc1  47224  cjnpoly  47337  f1cof1blem  47522  isubgr0uhgr  48349  uzlidlring  48711  ofaddmndmap  48819  dmatALTbas  48877  dflinc2  48886  fdivmpt  49016  zeroopropdlem  49717  incat  50076  aacllem  50276  amgmwlem  50277