Theorem inidm 4217

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

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

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954

This theorem is referenced by:  inindi  4225  inindir  4226  uneqin  4277  disjeq0  4454  ssdifeq0  4485  intsng  4988  xpindi  5831  xpindir  5832  resindm  6028  elidinxpid  6042  idinxpresid  6045  predidm  6324  offval2f  7681  fnfvof  7683  ofres  7685  offval2  7686  ofrfval2  7687  ofco  7689  offveq  7690  offveqb  7691  ofc1  7692  ofc2  7693  caofref  7695  caofrss  7702  caoftrn  7704  offsplitfpar  8101  suppssof1  8180  suppofssd  8184  suppofss1d  8185  suppofss2d  8186  fisn  9418  dffi3  9422  ofsubeq0  12205  ofnegsub  12206  ofsubge0  12207  seqof  14021  ofccat  14912  incexc  15779  sadeq  16409  smuval2  16419  smumul  16430  ressinbas  17186  pwsle  17434  pwsleval  17435  ghmplusg  19708  gsumzaddlem  19783  gsumzadd  19784  pwspjmhmmgpd  20134  lcomf  20503  crng2idl  20869  frlmipval  21325  frlmphllem  21326  frlmphl  21327  frlmsslsp  21342  frlmup1  21344  psrbaglesupp  21468  psrbaglesuppOLD  21469  psrbagaddcl  21472  psrbagaddclOLD  21473  psrbagcon  21474  psrbagconOLD  21475  psrbaglefi  21476  psrbaglefiOLD  21477  psrbagconf1o  21480  psrbagconf1oOLD  21481  gsumbagdiaglemOLD  21482  gsumbagdiaglem  21485  psraddcl  21493  psrvscacl  21503  psrlidm  21514  psrdi  21517  psrdir  21518  mplsubglem  21549  psrbagev1  21629  psrbagev1OLD  21630  evlslem3  21634  evlslem1  21636  mhpmulcl  21683  psrplusgpropd  21749  coe1add  21777  pf1ind  21865  mndvcl  21884  matplusgcell  21926  matsubgcell  21927  mat1dimscm  21968  baspartn  22448  indistopon  22495  epttop  22503  dissnlocfin  23024  ptbasin  23072  snfil  23359  tsmsadd  23642  ust0  23715  ustuqtop1  23737  rrxcph  24900  rrxds  24901  volun  25053  mbfmulc2lem  25155  mbfaddlem  25168  0pledm  25181  i1faddlem  25201  i1fmullem  25202  i1fadd  25203  i1fmul  25204  itg1addlem4  25207  itg1addlem4OLD  25208  i1fmulclem  25211  i1fmulc  25212  itg1lea  25221  itg1le  25222  mbfi1fseqlem5  25228  mbfi1flimlem  25231  mbfmullem2  25233  xrge0f  25240  itg2ge0  25244  itg2lea  25253  itg2mulclem  25255  itg2mulc  25256  itg2splitlem  25257  itg2split  25258  itg2monolem1  25259  itg2mono  25262  itg2i1fseqle  25263  itg2i1fseq  25264  itg2addlem  25267  itg2cnlem1  25270  dvaddf  25450  dvmulf  25451  dvcmulf  25453  dv11cn  25509  plyaddlem1  25718  plyaddlem  25720  coeeulem  25729  coeaddlem  25754  coemulc  25760  dgradd2  25773  dgrcolem2  25779  ofmulrt  25786  plydivlem3  25799  plydivlem4  25800  plydiveu  25802  plyrem  25809  vieta1lem2  25815  elqaalem3  25825  qaa  25827  jensenlem2  26481  jensen  26482  basellem7  26580  basellem9  26582  dchrmulcl  26741  chssoc  30736  chjidm  30760  mdslmd3i  31572  inin  31740  unidifsnne  31760  disjnf  31788  ofrn  31851  ofrn2  31852  ofresid  31854  offinsupp1  31939  gsumle  32229  tocyccntz  32290  islinds5  32468  ellspds  32469  evls1fpws  32634  ply1gsumz  32657  ply1degltdimlem  32695  fedgmullem1  32702  hauseqcn  32866  ofcof  33093  carsgclctunlem1  33304  carsgclctun  33308  sibfof  33327  plymul02  33545  signshf  33587  circlemethhgt  33643  msrid  34524  nepss  34675  bj-inrab2  35796  matunitlindflem1  36472  matunitlindflem2  36473  poimirlem1  36477  poimirlem2  36478  poimirlem3  36479  poimirlem4  36480  poimirlem6  36482  poimirlem7  36483  poimirlem8  36484  poimirlem10  36486  poimirlem11  36487  poimirlem12  36488  poimirlem16  36492  poimirlem17  36493  poimirlem19  36495  poimirlem20  36496  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem28  36504  poimirlem29  36505  poimirlem30  36506  poimirlem31  36507  poimirlem32  36508  broucube  36510  itg2addnclem  36527  itg2addnclem3  36529  itg2addnc  36530  ftc1anclem3  36551  ftc1anclem5  36553  ftc1anclem6  36554  ftc1anclem8  36556  blbnd  36643  lshpinN  37847  lfladdcl  37929  lflvscl  37935  ldualvaddval  37989  lclkrlem2e  40370  ofun  41055  mplmapghm  41125  evlsvvval  41132  fsuppind  41159  fsuppssind  41162  mhphf  41166  mzpclall  41450  mzpindd  41469  dgrsub2  41862  mpaaeu  41877  mendring  41919  ofoafo  42091  ofoacl  42092  ofoaid1  42093  ofoaid2  42094  ofoaass  42095  ofoacom  42096  naddcnff  42097  naddcnffo  42099  naddcnfcom  42101  naddcnfid1  42102  naddcnfass  42104  relexpaddss  42454  ntrkbimka  42774  clsk3nimkb  42776  caofcan  43067  ofmul12  43069  ofdivrec  43070  ofdivcan4  43071  ofdivdiv2  43072  expgrowth  43079  binomcxplemrat  43094  binomcxplemnotnn0  43100  disjf1  43865  dvsinax  44615  dvcosax  44628  dvdivcncf  44629  meadjun  45164  smfmulc1  45498  f1cof1blem  45770  uzlidlring  46780  ofaddmndmap  46972  mndpsuppss  47000  dmatALTbas  47035  dflinc2  47044  fdivmpt  47179  aacllem  47801  amgmwlem  47802