Theorem inidm 4172

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906

This theorem is used by:  inindi  4180  inindir  4181  uneqin  4235  disjeq0  4409  ssdifeq0  4442  intsng  4943  xpindi  5810  xpindir  5811  resindmOLD  6020  elidinxpid  6037  idinxpresid  6040  predidm  6329  offval2f  7708  fnfvof  7710  ofres  7712  offval2  7713  ofrfval2  7714  coof  7717  ofco  7718  offveq  7719  offveqb  7720  ofc1  7721  ofc2  7722  caofref  7724  caofrss  7732  caoftrn  7734  offsplitfpar  8130  suppssof1  8216  suppofssd  8220  suppofss1d  8221  suppofss2d  8222  fisn  9419  dffi3  9423  ofsubeq0  12317  ofnegsub  12318  ofsubge0  12319  seqof  14202  ofccat  15122  incexc  16006  sadeq  16642  smuval2  16652  smumul  16663  ressinbas  17423  pwsle  17664  pwsleval  17665  mndpsuppss  18959  mndvcl  18992  ghmplusg  20060  gsumzaddlem  20135  gsumzadd  20136  gsumle  20359  pwspjmhmmgpd  20557  lcomf  21176  crng2idl  21576  frlmipval  22085  frlmphllem  22086  frlmphl  22087  frlmsslsp  22102  frlmup1  22104  psrbaglesupp  22230  psrbagaddcl  22232  psrbagcon  22233  psrbaglefi  22234  psrbagleadd1  22236  psrbagconf1o  22237  gsumbagdiaglem  22239  psraddcl  22247  psrvscacl  22259  psrlidm  22269  psrdi  22272  psrdir  22273  psrascl  22286  mplsubglem  22306  psrbagev1  22386  evlslem3  22389  evlslem1  22391  evlsvvval  22402  mplmapghm  22431  mhpmulcl  22470  psdmplcl  22483  psdadd  22484  psdmul  22487  psdmvr  22490  psrplusgpropd  22553  coe1add  22583  pf1ind  22673  evls1fpws  22687  matplusgcell  22748  matsubgcell  22749  mat1dimscm  22790  matunitlindflem1  22994  matunitlindflem2  22995  baspartn  23272  indistopon  23319  epttop  23327  dissnlocfin  23848  ptbasin  23896  snfil  24183  tsmsadd  24466  ust0  24539  ustuqtop1  24560  rrxcph  25713  rrxds  25714  volun  25866  mbfmulc2lem  25968  mbfaddlem  25981  0pledm  25994  i1faddlem  26014  i1fmullem  26015  i1fadd  26016  i1fmul  26017  itg1addlem4  26020  i1fmulclem  26023  i1fmulc  26024  itg1lea  26033  itg1le  26034  mbfi1fseqlem5  26040  mbfi1flimlem  26043  mbfmullem2  26045  xrge0f  26052  itg2ge0  26056  itg2lea  26065  itg2mulclem  26067  itg2mulc  26068  itg2splitlem  26069  itg2split  26070  itg2monolem1  26071  itg2mono  26074  itg2i1fseqle  26075  itg2i1fseq  26076  itg2addlem  26079  itg2cnlem1  26082  dvaddf  26262  dvmulf  26263  dvcmulf  26265  dv11cn  26321  plyaddlem1  26532  plyaddlem  26534  coeeulem  26543  coeaddlem  26568  coemulc  26574  dgradd2  26587  dgrcolem2  26593  ofmulrt  26600  plymul02  26601  plydivlem3  26616  plydivlem4  26617  plydiveu  26619  plyrem  26626  rnplynfin  26630  vieta1lem2  26634  elqaalem3  26644  qaa  26647  jensenlem2  27315  jensen  27316  basellem7  27414  basellem9  27416  dchrmulcl  27576  chssoc  32098  chjidm  32122  mdslmd3i  32934  inin  33112  unidifsnne  33132  disjnf  33164  fnfvor  33203  ofrco  33204  ofrn  33233  ofrn2  33234  ofresid  33236  offinsupp1  33318  tocyccntz  33705  elrgspnlem1  33803  islinds5  33923  ellspds  33924  1arithidomlem2  34068  1arithidom  34069  ply1gsumz  34131  0mplrim  34146  selvply1rhmlemb  34151  selvply1rhmlem4  34155  mplvrpmrhm  34179  esplyind  34207  ply1degltdimlem  34254  fedgmullem1  34261  extdgfialglem2  34325  hauseqcn  34530  ofcof  34739  carsgclctunlem1  34949  carsgclctun  34953  sibfof  34972  signshf  35217  circlemethhgt  35272  msrid  36310  nepss  36483  bj-inrab2  37841  poimirlem1  38539  poimirlem2  38540  poimirlem4  38542  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  poimirlem10  38548  poimirlem11  38549  poimirlem12  38550  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem23  38561  poimirlem24  38562  poimirlem25  38563  poimirlem28  38566  poimirlem29  38567  poimirlem30  38568  poimirlem31  38569  poimirlem32  38570  broucube  38572  itg2addnclem  38589  itg2addnclem3  38591  itg2addnc  38592  ftc1anclem3  38613  ftc1anclem5  38615  ftc1anclem6  38616  ftc1anclem8  38618  blbnd  38721  disjimeceqim  39736  lshpinN  40046  lfladdcl  40128  lflvscl  40134  ldualvaddval  40188  lclkrlem2e  42568  ofun  43289  fsuppind  43618  fsuppssind  43621  mhphf  43625  mzpclall  43737  mzpindd  43756  dgrsub2  44136  mpaaeu  44151  mendring  44189  ofoafo  44357  ofoacl  44358  ofoaid1  44359  ofoaid2  44360  ofoaass  44361  ofoacom  44362  naddcnff  44363  naddcnffo  44365  naddcnfcom  44367  naddcnfid1  44368  naddcnfass  44370  relexpaddss  44717  ntrkbimka  45037  clsk3nimkb  45039  caofcan  45306  ofmul12  45308  ofdivrec  45309  ofdivcan4  45310  ofdivdiv2  45311  expgrowth  45318  binomcxplemrat  45333  binomcxplemnotnn0  45339  disjf1  46197  dvsinax  46922  dvcosax  46935  dvdivcncf  46936  meadjun  47471  smfmulc1  47805  cjnpoly  47938  f1cof1blem  48143  isubgr0uhgr  48970  uzlidlring  49331  ofaddmndmap  49454  dmatALTbas  49512  dflinc2  49521  fdivmpt  49651  zeroopropdlem  50349  incat  50708  aacllem  50938  veroquadmodzerod  50983  amgmwlem  50986