Theorem inidm 4183

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 565	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	ineqri 4169	1 ⊢ (𝐴 ∩ 𝐴) = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2106   ∩ cin 3912

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920

This theorem is referenced by:  inindi  4191  inindir  4192  uneqin  4243  disjeq0  4420  ssdifeq0  4449  intsng  4951  xpindi  5794  xpindir  5795  resindm  5991  elidinxpid  6003  idinxpresid  6006  predidm  6285  offval2f  7637  fnfvof  7639  ofres  7641  offval2  7642  ofrfval2  7643  ofco  7645  offveq  7646  offveqb  7647  ofc1  7648  ofc2  7649  caofref  7651  caofrss  7658  caoftrn  7660  offsplitfpar  8056  suppssof1  8135  suppofssd  8139  suppofss1d  8140  suppofss2d  8141  fisn  9372  dffi3  9376  ofsubeq0  12159  ofnegsub  12160  ofsubge0  12161  seqof  13975  ofccat  14866  incexc  15733  sadeq  16363  smuval2  16373  smumul  16384  ressinbas  17140  pwsle  17388  pwsleval  17389  ghmplusg  19638  gsumzaddlem  19712  gsumzadd  19713  pwspjmhmmgpd  20057  lcomf  20418  crng2idl  20768  frlmipval  21222  frlmphllem  21223  frlmphl  21224  frlmsslsp  21239  frlmup1  21241  psrbaglesupp  21363  psrbaglesuppOLD  21364  psrbagaddcl  21367  psrbagaddclOLD  21368  psrbagcon  21369  psrbagconOLD  21370  psrbaglefi  21371  psrbaglefiOLD  21372  psrbagconf1o  21375  psrbagconf1oOLD  21376  gsumbagdiaglemOLD  21377  gsumbagdiaglem  21380  psraddcl  21388  psrvscacl  21398  psrlidm  21409  psrdi  21412  psrdir  21413  mplsubglem  21442  psrbagev1  21522  psrbagev1OLD  21523  evlslem3  21527  evlslem1  21529  mhpmulcl  21576  psrplusgpropd  21644  coe1add  21672  pf1ind  21758  mndvcl  21777  matplusgcell  21819  matsubgcell  21820  mat1dimscm  21861  baspartn  22341  indistopon  22388  epttop  22396  dissnlocfin  22917  ptbasin  22965  snfil  23252  tsmsadd  23535  ust0  23608  ustuqtop1  23630  rrxcph  24793  rrxds  24794  volun  24946  mbfmulc2lem  25048  mbfaddlem  25061  0pledm  25074  i1faddlem  25094  i1fmullem  25095  i1fadd  25096  i1fmul  25097  itg1addlem4  25100  itg1addlem4OLD  25101  i1fmulclem  25104  i1fmulc  25105  itg1lea  25114  itg1le  25115  mbfi1fseqlem5  25121  mbfi1flimlem  25124  mbfmullem2  25126  xrge0f  25133  itg2ge0  25137  itg2lea  25146  itg2mulclem  25148  itg2mulc  25149  itg2splitlem  25150  itg2split  25151  itg2monolem1  25152  itg2mono  25155  itg2i1fseqle  25156  itg2i1fseq  25157  itg2addlem  25160  itg2cnlem1  25163  dvaddf  25343  dvmulf  25344  dvcmulf  25346  dv11cn  25402  plyaddlem1  25611  plyaddlem  25613  coeeulem  25622  coeaddlem  25647  coemulc  25653  dgradd2  25666  dgrcolem2  25672  ofmulrt  25679  plydivlem3  25692  plydivlem4  25693  plydiveu  25695  plyrem  25702  vieta1lem2  25708  elqaalem3  25718  qaa  25720  jensenlem2  26374  jensen  26375  basellem7  26473  basellem9  26475  dchrmulcl  26634  chssoc  30501  chjidm  30525  mdslmd3i  31337  inin  31506  unidifsnne  31527  disjnf  31555  ofrn  31622  ofrn2  31623  ofresid  31625  offinsupp1  31712  gsumle  32002  tocyccntz  32063  islinds5  32228  ellspds  32229  evls1fpws  32348  ply1gsumz  32368  ply1degltdimlem  32404  fedgmullem1  32411  hauseqcn  32568  ofcof  32795  carsgclctunlem1  33006  carsgclctun  33010  sibfof  33029  plymul02  33247  signshf  33289  circlemethhgt  33345  msrid  34226  nepss  34376  bj-inrab2  35471  matunitlindflem1  36147  matunitlindflem2  36148  poimirlem1  36152  poimirlem2  36153  poimirlem3  36154  poimirlem4  36155  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem23  36174  poimirlem24  36175  poimirlem25  36176  poimirlem28  36179  poimirlem29  36180  poimirlem30  36181  poimirlem31  36182  poimirlem32  36183  broucube  36185  itg2addnclem  36202  itg2addnclem3  36204  itg2addnc  36205  ftc1anclem3  36226  ftc1anclem5  36228  ftc1anclem6  36229  ftc1anclem8  36231  blbnd  36319  lshpinN  37524  lfladdcl  37606  lflvscl  37612  ldualvaddval  37666  lclkrlem2e  40047  ofun  40731  evlsbagval  40806  fsuppind  40823  fsuppssind  40826  mhphf  40829  mzpclall  41108  mzpindd  41127  dgrsub2  41520  mpaaeu  41535  mendring  41577  ofoafo  41749  ofoacl  41750  ofoaid1  41751  ofoaid2  41752  ofoaass  41753  ofoacom  41754  naddcnff  41755  naddcnffo  41757  naddcnfcom  41759  naddcnfid1  41760  naddcnfass  41762  relexpaddss  42112  ntrkbimka  42432  clsk3nimkb  42434  caofcan  42725  ofmul12  42727  ofdivrec  42728  ofdivcan4  42729  ofdivdiv2  42730  expgrowth  42737  binomcxplemrat  42752  binomcxplemnotnn0  42758  disjf1  43523  dvsinax  44274  dvcosax  44287  dvdivcncf  44288  meadjun  44823  smfmulc1  45157  f1cof1blem  45428  uzlidlring  46347  ofaddmndmap  46539  mndpsuppss  46567  dmatALTbas  46602  dflinc2  46611  fdivmpt  46746  aacllem  47368  amgmwlem  47369