Theorem inidm 4153

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

Syntax hints:   = wceq 1539   ∈ wcel 2107   ∩ cin 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895

This theorem is referenced by:  inindi  4161  inindir  4162  uneqin  4213  disjeq0  4390  ssdifeq0  4418  intsng  4917  xpindi  5745  xpindir  5746  resindm  5943  elidinxpid  5955  idinxpresid  5958  predidm  6233  offval2f  7557  fnfvof  7559  ofres  7561  offval2  7562  ofrfval2  7563  ofco  7565  offveq  7566  offveqb  7567  ofc1  7568  ofc2  7569  caofref  7571  caofrss  7578  caoftrn  7580  offsplitfpar  7969  suppssof1  8024  suppofssd  8028  suppofss1d  8029  suppofss2d  8030  fisn  9195  dffi3  9199  ofsubeq0  11979  ofnegsub  11980  ofsubge0  11981  seqof  13789  ofccat  14689  incexc  15558  sadeq  16188  smuval2  16198  smumul  16209  ressinbas  16964  pwsle  17212  pwsleval  17213  ghmplusg  19456  gsumzaddlem  19531  gsumzadd  19532  lcomf  20171  crng2idl  20519  frlmipval  20995  frlmphllem  20996  frlmphl  20997  frlmsslsp  21012  frlmup1  21014  psrbaglesupp  21136  psrbaglesuppOLD  21137  psrbagaddcl  21140  psrbagaddclOLD  21141  psrbagcon  21142  psrbagconOLD  21143  psrbaglefi  21144  psrbaglefiOLD  21145  psrbagconf1o  21148  psrbagconf1oOLD  21149  gsumbagdiaglemOLD  21150  gsumbagdiaglem  21153  psraddcl  21161  psrvscacl  21171  psrlidm  21181  psrdi  21184  psrdir  21185  mplsubglem  21214  psrbagev1  21294  psrbagev1OLD  21295  evlslem3  21299  evlslem1  21301  mhpmulcl  21348  psrplusgpropd  21416  coe1add  21444  pf1ind  21530  mndvcl  21549  matplusgcell  21591  matsubgcell  21592  mat1dimscm  21633  baspartn  22113  indistopon  22160  epttop  22168  dissnlocfin  22689  ptbasin  22737  snfil  23024  tsmsadd  23307  ust0  23380  ustuqtop1  23402  rrxcph  24565  rrxds  24566  volun  24718  mbfmulc2lem  24820  mbfaddlem  24833  0pledm  24846  i1faddlem  24866  i1fmullem  24867  i1fadd  24868  i1fmul  24869  itg1addlem4  24872  itg1addlem4OLD  24873  i1fmulclem  24876  i1fmulc  24877  itg1lea  24886  itg1le  24887  mbfi1fseqlem5  24893  mbfi1flimlem  24896  mbfmullem2  24898  xrge0f  24905  itg2ge0  24909  itg2lea  24918  itg2mulclem  24920  itg2mulc  24921  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itg2mono  24927  itg2i1fseqle  24928  itg2i1fseq  24929  itg2addlem  24932  itg2cnlem1  24935  dvaddf  25115  dvmulf  25116  dvcmulf  25118  dv11cn  25174  plyaddlem1  25383  plyaddlem  25385  coeeulem  25394  coeaddlem  25419  coemulc  25425  dgradd2  25438  dgrcolem2  25444  ofmulrt  25451  plydivlem3  25464  plydivlem4  25465  plydiveu  25467  plyrem  25474  vieta1lem2  25480  elqaalem3  25490  qaa  25492  jensenlem2  26146  jensen  26147  basellem7  26245  basellem9  26247  dchrmulcl  26406  chssoc  29867  chjidm  29891  mdslmd3i  30703  inin  30871  unidifsnne  30893  disjnf  30918  ofrn  30985  ofrn2  30986  ofresid  30988  offinsupp1  31071  gsumle  31359  tocyccntz  31420  islinds5  31572  ellspds  31573  fedgmullem1  31719  hauseqcn  31857  ofcof  32084  carsgclctunlem1  32293  carsgclctun  32297  sibfof  32316  plymul02  32534  signshf  32576  circlemethhgt  32632  msrid  33516  nepss  33671  bj-inrab2  35125  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  broucube  35820  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  ftc1anclem3  35861  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem8  35866  blbnd  35954  lshpinN  37010  lfladdcl  37092  lflvscl  37098  ldualvaddval  37152  lclkrlem2e  39532  ofun  40218  pwspjmhmmgpd  40274  evlsbagval  40282  fsuppind  40286  fsuppssind  40289  mhphf  40292  mzpclall  40556  mzpindd  40575  dgrsub2  40967  mpaaeu  40982  mendring  41024  relexpaddss  41333  ntrkbimka  41655  clsk3nimkb  41657  caofcan  41948  ofmul12  41950  ofdivrec  41951  ofdivcan4  41952  ofdivdiv2  41953  expgrowth  41960  binomcxplemrat  41975  binomcxplemnotnn0  41981  disjf1  42727  dvsinax  43461  dvcosax  43474  dvdivcncf  43475  meadjun  44007  smfmulc1  44341  f1cof1blem  44579  uzlidlring  45498  ofaddmndmap  45690  mndpsuppss  45718  dmatALTbas  45753  dflinc2  45762  fdivmpt  45897  aacllem  46516  amgmwlem  46517