Theorem inidm 4145

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

Syntax hints:   = wceq 1538   ∈ wcel 2111   ∩ cin 3880

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888

This theorem is referenced by:  inindi  4153  inindir  4154  uneqin  4205  disjeq0  4363  ssdifeq0  4390  intsng  4873  xpindi  5668  xpindir  5669  resindm  5867  elidinxpid  5879  idinxpresid  5882  predidm  6138  offval2f  7401  fnfvof  7403  ofres  7405  offval2  7406  ofrfval2  7407  ofco  7409  offveq  7410  offveqb  7411  ofc1  7412  ofc2  7413  caofref  7415  caofrss  7422  caoftrn  7424  offsplitfpar  7798  suppssof1  7846  suppofssd  7850  suppofss1d  7851  suppofss2d  7852  fisn  8875  dffi3  8879  ofsubeq0  11622  ofnegsub  11623  ofsubge0  11624  seqof  13423  ofccat  14320  incexc  15184  sadeq  15811  smuval2  15821  smumul  15832  ressinbas  16552  pwsle  16757  pwsleval  16758  ghmplusg  18959  gsumzaddlem  19034  gsumzadd  19035  lcomf  19666  lcomfsupp  19667  crng2idl  20005  frlmipval  20468  frlmphllem  20469  frlmphl  20470  frlmsslsp  20485  frlmup1  20487  psrbaglesupp  20606  psrbagaddcl  20608  psrbagcon  20609  psrbaglefi  20610  psrbagconf1o  20612  gsumbagdiaglem  20613  psraddcl  20621  psrvscacl  20631  psrlidm  20641  psrdi  20644  psrdir  20645  mplsubglem  20672  psrbagev1  20749  evlslem3  20752  evlslem1  20754  psrplusgpropd  20865  coe1add  20893  pf1ind  20979  mndvcl  20998  matplusgcell  21038  matsubgcell  21039  mat1dimscm  21080  baspartn  21559  indistopon  21606  epttop  21614  dissnlocfin  22134  ptbasin  22182  snfil  22469  tsmsadd  22752  ust0  22825  ustuqtop1  22847  rrxcph  23996  rrxds  23997  volun  24149  mbfmulc2lem  24251  mbfaddlem  24264  0pledm  24277  i1faddlem  24297  i1fmullem  24298  i1fadd  24299  i1fmul  24300  itg1addlem4  24303  i1fmulclem  24306  i1fmulc  24307  itg1lea  24316  itg1le  24317  mbfi1fseqlem5  24323  mbfi1flimlem  24326  mbfmullem2  24328  xrge0f  24335  itg2ge0  24339  itg2lea  24348  itg2mulclem  24350  itg2mulc  24351  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itg2mono  24357  itg2i1fseqle  24358  itg2i1fseq  24359  itg2addlem  24362  itg2cnlem1  24365  dvaddf  24545  dvmulf  24546  dvcmulf  24548  dv11cn  24604  plyaddlem1  24810  plyaddlem  24812  coeeulem  24821  coeaddlem  24846  coemulc  24852  dgradd2  24865  dgrcolem2  24871  ofmulrt  24878  plydivlem3  24891  plydivlem4  24892  plydiveu  24894  plyrem  24901  vieta1lem2  24907  elqaalem3  24917  qaa  24919  jensenlem2  25573  jensen  25574  basellem7  25672  basellem9  25674  dchrmulcl  25833  chssoc  29279  chjidm  29303  mdslmd3i  30115  inin  30286  unidifsnne  30308  disjnf  30333  ofrn  30400  ofrn2  30401  ofresid  30403  offinsupp1  30489  gsumle  30775  tocyccntz  30836  islinds5  30983  ellspds  30984  fedgmullem1  31113  hauseqcn  31251  ofcof  31476  carsgclctunlem1  31685  carsgclctun  31689  sibfof  31708  plymul02  31926  signshf  31968  circlemethhgt  32024  msrid  32905  nepss  33061  bj-inrab2  34370  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem28  35085  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  broucube  35091  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  ftc1anclem3  35132  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem8  35137  blbnd  35225  lshpinN  36285  lfladdcl  36367  lflvscl  36373  ldualvaddval  36427  lclkrlem2e  38807  ofun  39416  fsuppind  39456  fsuppssind  39459  mzpclall  39668  mzpindd  39687  dgrsub2  40079  mpaaeu  40094  mendring  40136  relexpaddss  40419  ntrkbimka  40741  clsk3nimkb  40743  caofcan  41027  ofmul12  41029  ofdivrec  41030  ofdivcan4  41031  ofdivdiv2  41032  expgrowth  41039  binomcxplemrat  41054  binomcxplemnotnn0  41060  disjf1  41809  dvsinax  42555  dvcosax  42568  dvdivcncf  42569  meadjun  43101  smfmulc1  43428  uzlidlring  44553  ofaddmndmap  44745  mndpsuppss  44773  mndpfsupp  44778  dmatALTbas  44810  dflinc2  44819  fdivmpt  44954  aacllem  45329  amgmwlem  45330