Theorem inidm 4180

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

Syntax hints:   = wceq 1562   ∈ wcel 2144   ∩ cin 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-in 3913

This theorem is referenced by:  inindi  4188  inindir  4189  uneqin  4243  disjeq0  4412  ssdifeq0  4442  intsng  4943  xpindi  5807  xpindir  5808  resindmOLD  6019  elidinxpid  6036  idinxpresid  6039  predidm  6315  offval2f  7677  fnfvof  7679  ofres  7681  offval2  7682  ofrfval2  7683  coof  7686  ofco  7687  offveq  7688  offveqb  7689  ofc1  7690  ofc2  7691  caofref  7693  caofrss  7701  caoftrn  7703  offsplitfpar  8100  suppssof1  8181  suppofssd  8185  suppofss1d  8186  suppofss2d  8187  fisn  9375  dffi3  9379  ofsubeq0  12194  ofnegsub  12195  ofsubge0  12196  seqof  14074  ofccat  14984  incexc  15869  sadeq  16508  smuval2  16518  smumul  16529  ressinbas  17283  pwsle  17524  pwsleval  17525  mndpsuppss  18801  mndvcl  18833  ghmplusg  19888  gsumzaddlem  19963  gsumzadd  19964  gsumle  20187  pwspjmhmmgpd  20378  lcomf  20970  crng2idl  21353  frlmipval  21833  frlmphllem  21834  frlmphl  21835  frlmsslsp  21850  frlmup1  21852  psrbaglesupp  21976  psrbagaddcl  21978  psrbagcon  21979  psrbaglefi  21980  psrbagleadd1  21982  psrbagconf1o  21983  gsumbagdiaglem  21985  psraddcl  21993  psrvscacl  22005  psrlidm  22015  psrdi  22018  psrdir  22019  psrascl  22032  mplsubglem  22052  psrbagev1  22132  evlslem3  22135  evlslem1  22137  evlsvvval  22148  mplmapghm  22177  mhpmulcl  22216  psdmplcl  22229  psdadd  22230  psdmul  22233  psdmvr  22236  psrplusgpropd  22299  coe1add  22329  pf1ind  22420  evls1fpws  22434  matplusgcell  22495  matsubgcell  22496  mat1dimscm  22537  baspartn  23016  indistopon  23063  epttop  23071  dissnlocfin  23591  ptbasin  23639  snfil  23926  tsmsadd  24209  ust0  24282  ustuqtop1  24303  rrxcph  25456  rrxds  25457  volun  25609  mbfmulc2lem  25711  mbfaddlem  25724  0pledm  25737  i1faddlem  25757  i1fmullem  25758  i1fadd  25759  i1fmul  25760  itg1addlem4  25763  i1fmulclem  25766  i1fmulc  25767  itg1lea  25776  itg1le  25777  mbfi1fseqlem5  25783  mbfi1flimlem  25786  mbfmullem2  25788  xrge0f  25795  itg2ge0  25799  itg2lea  25808  itg2mulclem  25810  itg2mulc  25811  itg2splitlem  25812  itg2split  25813  itg2monolem1  25814  itg2mono  25817  itg2i1fseqle  25818  itg2i1fseq  25819  itg2addlem  25822  itg2cnlem1  25825  dvaddf  26006  dvmulf  26007  dvcmulf  26009  dv11cn  26065  plyaddlem1  26275  plyaddlem  26277  coeeulem  26286  coeaddlem  26311  coemulc  26317  dgradd2  26330  dgrcolem2  26336  ofmulrt  26345  plymul02  26346  plydivlem3  26361  plydivlem4  26362  plydiveu  26364  plyrem  26371  vieta1lem2  26377  elqaalem3  26387  qaa  26389  jensenlem2  27054  jensen  27055  basellem7  27153  basellem9  27155  dchrmulcl  27315  chssoc  31701  chjidm  31725  mdslmd3i  32537  inin  32717  unidifsnne  32737  disjnf  32772  fnfvor  32813  ofrco  32814  ofrn  32843  ofrn2  32844  ofresid  32846  offinsupp1  32930  tocyccntz  33326  elrgspnlem1  33425  islinds5  33555  ellspds  33556  1arithidomlem2  33734  1arithidom  33735  ply1gsumz  33797  0mplrim  33813  selvply1rhmlemb  33818  selvply1rhmlem4  33822  mplvrpmrhm  33846  esplyind  33874  ply1degltdimlem  33921  fedgmullem1  33928  extdgfialglem2  33992  hauseqcn  34197  ofcof  34406  carsgclctunlem1  34616  carsgclctun  34620  sibfof  34639  signshf  34884  circlemethhgt  34939  msrid  35900  nepss  36073  bj-inrab2  37418  matunitlindflem1  38120  matunitlindflem2  38121  poimirlem1  38125  poimirlem2  38126  poimirlem4  38128  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem10  38134  poimirlem11  38135  poimirlem12  38136  poimirlem16  38140  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  poimirlem23  38147  poimirlem24  38148  poimirlem25  38149  poimirlem28  38152  poimirlem29  38153  poimirlem30  38154  poimirlem31  38155  poimirlem32  38156  broucube  38158  itg2addnclem  38175  itg2addnclem3  38177  itg2addnc  38178  ftc1anclem3  38199  ftc1anclem5  38201  ftc1anclem6  38202  ftc1anclem8  38204  blbnd  38291  disjimeceqim  39308  lshpinN  39618  lfladdcl  39700  lflvscl  39706  ldualvaddval  39760  lclkrlem2e  42140  ofun  42859  fsuppind  43177  fsuppssind  43180  mhphf  43184  mzpclall  43313  mzpindd  43332  dgrsub2  43717  mpaaeu  43732  mendring  43770  ofoafo  43938  ofoacl  43939  ofoaid1  43940  ofoaid2  43941  ofoaass  43942  ofoacom  43943  naddcnff  43944  naddcnffo  43946  naddcnfcom  43948  naddcnfid1  43949  naddcnfass  43951  relexpaddss  44299  ntrkbimka  44619  clsk3nimkb  44621  caofcan  44904  ofmul12  44906  ofdivrec  44907  ofdivcan4  44908  ofdivdiv2  44909  expgrowth  44916  binomcxplemrat  44931  binomcxplemnotnn0  44937  disjf1  45766  dvsinax  46492  dvcosax  46505  dvdivcncf  46506  meadjun  47041  smfmulc1  47375  cjnpoly  47488  f1cof1blem  47673  isubgr0uhgr  48500  uzlidlring  48862  ofaddmndmap  48970  dmatALTbas  49028  dflinc2  49037  fdivmpt  49167  zeroopropdlem  49868  incat  50227  aacllem  50427  amgmwlem  50428