Theorem inidm 4174

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

Syntax hints:   = wceq 1541   ∈ wcel 2111   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  inindi  4182  inindir  4183  uneqin  4236  disjeq0  4403  ssdifeq0  4434  intsng  4931  xpindi  5772  xpindir  5773  resindm  5978  elidinxpid  5993  idinxpresid  5996  predidm  6273  offval2f  7625  fnfvof  7627  ofres  7629  offval2  7630  ofrfval2  7631  coof  7634  ofco  7635  offveq  7636  offveqb  7637  ofc1  7638  ofc2  7639  caofref  7641  caofrss  7649  caoftrn  7651  offsplitfpar  8049  suppssof1  8129  suppofssd  8133  suppofss1d  8134  suppofss2d  8135  fisn  9311  dffi3  9315  ofsubeq0  12122  ofnegsub  12123  ofsubge0  12124  seqof  13966  ofccat  14876  incexc  15744  sadeq  16383  smuval2  16393  smumul  16404  ressinbas  17156  pwsle  17396  pwsleval  17397  mndpsuppss  18673  mndvcl  18705  ghmplusg  19758  gsumzaddlem  19833  gsumzadd  19834  gsumle  20057  pwspjmhmmgpd  20246  lcomf  20834  crng2idl  21218  frlmipval  21716  frlmphllem  21717  frlmphl  21718  frlmsslsp  21733  frlmup1  21735  psrbaglesupp  21859  psrbagaddcl  21861  psrbagcon  21862  psrbaglefi  21863  psrbagleadd1  21865  psrbagconf1o  21866  gsumbagdiaglem  21867  psraddcl  21875  psraddclOLD  21876  psrvscacl  21888  psrlidm  21899  psrdi  21902  psrdir  21903  psrascl  21916  mplsubglem  21936  psrbagev1  22012  evlslem3  22015  evlslem1  22017  mhpmulcl  22064  psdmplcl  22077  psdadd  22078  psdmul  22081  psdmvr  22084  psrplusgpropd  22148  coe1add  22178  pf1ind  22270  evls1fpws  22284  matplusgcell  22348  matsubgcell  22349  mat1dimscm  22390  baspartn  22869  indistopon  22916  epttop  22924  dissnlocfin  23444  ptbasin  23492  snfil  23779  tsmsadd  24062  ust0  24135  ustuqtop1  24156  rrxcph  25319  rrxds  25320  volun  25473  mbfmulc2lem  25575  mbfaddlem  25588  0pledm  25601  i1faddlem  25621  i1fmullem  25622  i1fadd  25623  i1fmul  25624  itg1addlem4  25627  i1fmulclem  25630  i1fmulc  25631  itg1lea  25640  itg1le  25641  mbfi1fseqlem5  25647  mbfi1flimlem  25650  mbfmullem2  25652  xrge0f  25659  itg2ge0  25663  itg2lea  25672  itg2mulclem  25674  itg2mulc  25675  itg2splitlem  25676  itg2split  25677  itg2monolem1  25678  itg2mono  25681  itg2i1fseqle  25682  itg2i1fseq  25683  itg2addlem  25686  itg2cnlem1  25689  dvaddf  25872  dvmulf  25873  dvcmulf  25875  dv11cn  25933  plyaddlem1  26145  plyaddlem  26147  coeeulem  26156  coeaddlem  26181  coemulc  26187  dgradd2  26201  dgrcolem2  26207  ofmulrt  26216  plydivlem3  26230  plydivlem4  26231  plydiveu  26233  plyrem  26240  vieta1lem2  26246  elqaalem3  26256  qaa  26258  jensenlem2  26925  jensen  26926  basellem7  27024  basellem9  27026  dchrmulcl  27187  chssoc  31476  chjidm  31500  mdslmd3i  32312  inin  32496  unidifsnne  32516  disjnf  32550  fnfvor  32592  ofrco  32593  ofrn  32621  ofrn2  32622  ofresid  32624  offinsupp1  32709  tocyccntz  33113  elrgspnlem1  33209  islinds5  33332  ellspds  33333  1arithidomlem2  33501  1arithidom  33502  ply1gsumz  33559  mplvrpmrhm  33577  ply1degltdimlem  33635  fedgmullem1  33642  extdgfialglem2  33706  hauseqcn  33911  ofcof  34120  carsgclctunlem1  34330  carsgclctun  34334  sibfof  34353  plymul02  34559  signshf  34601  circlemethhgt  34656  msrid  35589  nepss  35762  bj-inrab2  36972  matunitlindflem1  37666  matunitlindflem2  37667  poimirlem1  37671  poimirlem2  37672  poimirlem3  37673  poimirlem4  37674  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem23  37693  poimirlem24  37694  poimirlem25  37695  poimirlem28  37698  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  broucube  37704  itg2addnclem  37721  itg2addnclem3  37723  itg2addnc  37724  ftc1anclem3  37745  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem8  37750  blbnd  37837  lshpinN  39098  lfladdcl  39180  lflvscl  39186  ldualvaddval  39240  lclkrlem2e  41620  ofun  42339  mplmapghm  42659  evlsvvval  42666  fsuppind  42693  fsuppssind  42696  mhphf  42700  mzpclall  42830  mzpindd  42849  dgrsub2  43238  mpaaeu  43253  mendring  43291  ofoafo  43459  ofoacl  43460  ofoaid1  43461  ofoaid2  43462  ofoaass  43463  ofoacom  43464  naddcnff  43465  naddcnffo  43467  naddcnfcom  43469  naddcnfid1  43470  naddcnfass  43472  relexpaddss  43821  ntrkbimka  44141  clsk3nimkb  44143  caofcan  44426  ofmul12  44428  ofdivrec  44429  ofdivcan4  44430  ofdivdiv2  44431  expgrowth  44438  binomcxplemrat  44453  binomcxplemnotnn0  44459  disjf1  45290  dvsinax  46021  dvcosax  46034  dvdivcncf  46035  meadjun  46570  smfmulc1  46904  cjnpoly  46999  f1cof1blem  47184  isubgr0uhgr  47983  uzlidlring  48345  ofaddmndmap  48453  dmatALTbas  48512  dflinc2  48521  fdivmpt  48651  zeroopropdlem  49353  incat  49712  aacllem  49912  amgmwlem  49913