Theorem inidm 4168

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  inindi  4176  inindir  4177  uneqin  4230  disjeq0  4397  ssdifeq0  4427  intsng  4926  xpindi  5784  xpindir  5785  resindm  5991  elidinxpid  6006  idinxpresid  6009  predidm  6286  offval2f  7641  fnfvof  7643  ofres  7645  offval2  7646  ofrfval2  7647  coof  7650  ofco  7651  offveq  7652  offveqb  7653  ofc1  7654  ofc2  7655  caofref  7657  caofrss  7665  caoftrn  7667  offsplitfpar  8064  suppssof1  8144  suppofssd  8148  suppofss1d  8149  suppofss2d  8150  fisn  9335  dffi3  9339  ofsubeq0  12151  ofnegsub  12152  ofsubge0  12153  seqof  14016  ofccat  14926  incexc  15797  sadeq  16436  smuval2  16446  smumul  16457  ressinbas  17210  pwsle  17451  pwsleval  17452  mndpsuppss  18728  mndvcl  18760  ghmplusg  19816  gsumzaddlem  19891  gsumzadd  19892  gsumle  20115  pwspjmhmmgpd  20302  lcomf  20891  crng2idl  21275  frlmipval  21773  frlmphllem  21774  frlmphl  21775  frlmsslsp  21790  frlmup1  21792  psrbaglesupp  21916  psrbagaddcl  21918  psrbagcon  21919  psrbaglefi  21920  psrbagleadd1  21922  psrbagconf1o  21923  gsumbagdiaglem  21924  psraddcl  21932  psrvscacl  21944  psrlidm  21954  psrdi  21957  psrdir  21958  psrascl  21971  mplsubglem  21991  psrbagev1  22069  evlslem3  22072  evlslem1  22074  evlsvvval  22085  mhpmulcl  22129  psdmplcl  22142  psdadd  22143  psdmul  22146  psdmvr  22149  psrplusgpropd  22213  coe1add  22243  pf1ind  22334  evls1fpws  22348  matplusgcell  22412  matsubgcell  22413  mat1dimscm  22454  baspartn  22933  indistopon  22980  epttop  22988  dissnlocfin  23508  ptbasin  23556  snfil  23843  tsmsadd  24126  ust0  24199  ustuqtop1  24220  rrxcph  25373  rrxds  25374  volun  25526  mbfmulc2lem  25628  mbfaddlem  25641  0pledm  25654  i1faddlem  25674  i1fmullem  25675  i1fadd  25676  i1fmul  25677  itg1addlem4  25680  i1fmulclem  25683  i1fmulc  25684  itg1lea  25693  itg1le  25694  mbfi1fseqlem5  25700  mbfi1flimlem  25703  mbfmullem2  25705  xrge0f  25712  itg2ge0  25716  itg2lea  25725  itg2mulclem  25727  itg2mulc  25728  itg2splitlem  25729  itg2split  25730  itg2monolem1  25731  itg2mono  25734  itg2i1fseqle  25735  itg2i1fseq  25736  itg2addlem  25739  itg2cnlem1  25742  dvaddf  25923  dvmulf  25924  dvcmulf  25926  dv11cn  25982  plyaddlem1  26192  plyaddlem  26194  coeeulem  26203  coeaddlem  26228  coemulc  26234  dgradd2  26247  dgrcolem2  26253  ofmulrt  26262  plydivlem3  26276  plydivlem4  26277  plydiveu  26279  plyrem  26286  vieta1lem2  26292  elqaalem3  26302  qaa  26304  jensenlem2  26969  jensen  26970  basellem7  27068  basellem9  27070  dchrmulcl  27230  chssoc  31586  chjidm  31610  mdslmd3i  32422  inin  32605  unidifsnne  32625  disjnf  32659  fnfvor  32701  ofrco  32702  ofrn  32731  ofrn2  32732  ofresid  32734  offinsupp1  32818  tocyccntz  33224  elrgspnlem1  33322  islinds5  33446  ellspds  33447  1arithidomlem2  33615  1arithidom  33616  ply1gsumz  33678  mplvrpmrhm  33710  esplyind  33738  ply1degltdimlem  33786  fedgmullem1  33793  extdgfialglem2  33857  hauseqcn  34062  ofcof  34271  carsgclctunlem1  34481  carsgclctun  34485  sibfof  34504  plymul02  34710  signshf  34752  circlemethhgt  34807  msrid  35747  nepss  35920  bj-inrab2  37255  matunitlindflem1  37955  matunitlindflem2  37956  poimirlem1  37960  poimirlem2  37961  poimirlem3  37962  poimirlem4  37963  poimirlem6  37965  poimirlem7  37966  poimirlem8  37967  poimirlem10  37969  poimirlem11  37970  poimirlem12  37971  poimirlem16  37975  poimirlem17  37976  poimirlem19  37978  poimirlem20  37979  poimirlem23  37982  poimirlem24  37983  poimirlem25  37984  poimirlem28  37987  poimirlem29  37988  poimirlem30  37989  poimirlem31  37990  poimirlem32  37991  broucube  37993  itg2addnclem  38010  itg2addnclem3  38012  itg2addnc  38013  ftc1anclem3  38034  ftc1anclem5  38036  ftc1anclem6  38037  ftc1anclem8  38039  blbnd  38126  disjimeceqim  39143  lshpinN  39453  lfladdcl  39535  lflvscl  39541  ldualvaddval  39595  lclkrlem2e  41975  ofun  42695  mplmapghm  43015  fsuppind  43041  fsuppssind  43044  mhphf  43048  mzpclall  43177  mzpindd  43196  dgrsub2  43585  mpaaeu  43600  mendring  43638  ofoafo  43806  ofoacl  43807  ofoaid1  43808  ofoaid2  43809  ofoaass  43810  ofoacom  43811  naddcnff  43812  naddcnffo  43814  naddcnfcom  43816  naddcnfid1  43817  naddcnfass  43819  relexpaddss  44167  ntrkbimka  44487  clsk3nimkb  44489  caofcan  44772  ofmul12  44774  ofdivrec  44775  ofdivcan4  44776  ofdivdiv2  44777  expgrowth  44784  binomcxplemrat  44799  binomcxplemnotnn0  44805  disjf1  45635  dvsinax  46363  dvcosax  46376  dvdivcncf  46377  meadjun  46912  smfmulc1  47246  cjnpoly  47353  f1cof1blem  47538  isubgr0uhgr  48365  uzlidlring  48727  ofaddmndmap  48835  dmatALTbas  48893  dflinc2  48902  fdivmpt  49032  zeroopropdlem  49733  incat  50092  aacllem  50292  amgmwlem  50293