Theorem inidm 4187

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

Syntax hints:   = wceq 1567   ∈ wcel 2149   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  inindi  4195  inindir  4196  uneqin  4250  disjeq0  4422  ssdifeq0  4452  intsng  4952  xpindi  5820  xpindir  5821  resindmOLD  6031  elidinxpid  6048  idinxpresid  6051  predidm  6328  offval2f  7690  fnfvof  7692  ofres  7694  offval2  7695  ofrfval2  7696  coof  7699  ofco  7700  offveq  7701  offveqb  7702  ofc1  7703  ofc2  7704  caofref  7706  caofrss  7714  caoftrn  7716  offsplitfpar  8114  suppssof1  8195  suppofssd  8199  suppofss1d  8200  suppofss2d  8201  fisn  9387  dffi3  9391  ofsubeq0  12215  ofnegsub  12216  ofsubge0  12217  seqof  14095  ofccat  15006  incexc  15891  sadeq  16530  smuval2  16540  smumul  16551  ressinbas  17305  pwsle  17546  pwsleval  17547  mndpsuppss  18823  mndvcl  18855  ghmplusg  19916  gsumzaddlem  19991  gsumzadd  19992  gsumle  20215  pwspjmhmmgpd  20409  lcomf  21000  crng2idl  21391  frlmipval  21898  frlmphllem  21899  frlmphl  21900  frlmsslsp  21915  frlmup1  21917  psrbaglesupp  22041  psrbagaddcl  22043  psrbagcon  22044  psrbaglefi  22045  psrbagleadd1  22047  psrbagconf1o  22048  gsumbagdiaglem  22050  psraddcl  22058  psrvscacl  22070  psrlidm  22080  psrdi  22083  psrdir  22084  psrascl  22097  mplsubglem  22117  psrbagev1  22197  evlslem3  22200  evlslem1  22202  evlsvvval  22213  mplmapghm  22242  mhpmulcl  22281  psdmplcl  22294  psdadd  22295  psdmul  22298  psdmvr  22301  psrplusgpropd  22364  coe1add  22394  pf1ind  22484  evls1fpws  22498  matplusgcell  22559  matsubgcell  22560  mat1dimscm  22601  baspartn  23080  indistopon  23127  epttop  23135  dissnlocfin  23655  ptbasin  23703  snfil  23990  tsmsadd  24273  ust0  24346  ustuqtop1  24367  rrxcph  25520  rrxds  25521  volun  25673  mbfmulc2lem  25775  mbfaddlem  25788  0pledm  25801  i1faddlem  25821  i1fmullem  25822  i1fadd  25823  i1fmul  25824  itg1addlem4  25827  i1fmulclem  25830  i1fmulc  25831  itg1lea  25840  itg1le  25841  mbfi1fseqlem5  25847  mbfi1flimlem  25850  mbfmullem2  25852  xrge0f  25859  itg2ge0  25863  itg2lea  25872  itg2mulclem  25874  itg2mulc  25875  itg2splitlem  25876  itg2split  25877  itg2monolem1  25878  itg2mono  25881  itg2i1fseqle  25882  itg2i1fseq  25883  itg2addlem  25886  itg2cnlem1  25889  dvaddf  26070  dvmulf  26071  dvcmulf  26073  dv11cn  26129  plyaddlem1  26339  plyaddlem  26341  coeeulem  26350  coeaddlem  26375  coemulc  26381  dgradd2  26394  dgrcolem2  26400  ofmulrt  26409  plymul02  26410  plydivlem3  26425  plydivlem4  26426  plydiveu  26428  plyrem  26435  vieta1lem2  26441  elqaalem3  26451  qaa  26453  jensenlem2  27118  jensen  27119  basellem7  27217  basellem9  27219  dchrmulcl  27379  chssoc  31789  chjidm  31813  mdslmd3i  32625  inin  32803  unidifsnne  32823  disjnf  32856  fnfvor  32895  ofrco  32896  ofrn  32925  ofrn2  32926  ofresid  32928  offinsupp1  33012  tocyccntz  33405  elrgspnlem1  33503  islinds5  33625  ellspds  33626  1arithidomlem2  33771  1arithidom  33772  ply1gsumz  33834  0mplrim  33849  selvply1rhmlemb  33854  selvply1rhmlem4  33858  mplvrpmrhm  33882  esplyind  33910  ply1degltdimlem  33957  fedgmullem1  33964  extdgfialglem2  34028  hauseqcn  34233  ofcof  34442  carsgclctunlem1  34652  carsgclctun  34656  sibfof  34675  signshf  34920  circlemethhgt  34975  msrid  35970  nepss  36143  bj-inrab2  37486  matunitlindflem1  38189  matunitlindflem2  38190  poimirlem1  38194  poimirlem2  38195  poimirlem4  38197  poimirlem6  38199  poimirlem7  38200  poimirlem8  38201  poimirlem10  38203  poimirlem11  38204  poimirlem12  38205  poimirlem16  38209  poimirlem17  38210  poimirlem19  38212  poimirlem20  38213  poimirlem23  38216  poimirlem24  38217  poimirlem25  38218  poimirlem28  38221  poimirlem29  38222  poimirlem30  38223  poimirlem31  38224  poimirlem32  38225  broucube  38227  itg2addnclem  38244  itg2addnclem3  38246  itg2addnc  38247  ftc1anclem3  38268  ftc1anclem5  38270  ftc1anclem6  38271  ftc1anclem8  38273  blbnd  38360  disjimeceqim  39377  lshpinN  39687  lfladdcl  39769  lflvscl  39775  ldualvaddval  39829  lclkrlem2e  42209  ofun  42930  fsuppind  43248  fsuppssind  43251  mhphf  43255  mzpclall  43384  mzpindd  43403  dgrsub2  43788  mpaaeu  43803  mendring  43841  ofoafo  44009  ofoacl  44010  ofoaid1  44011  ofoaid2  44012  ofoaass  44013  ofoacom  44014  naddcnff  44015  naddcnffo  44017  naddcnfcom  44019  naddcnfid1  44020  naddcnfass  44022  relexpaddss  44370  ntrkbimka  44690  clsk3nimkb  44692  caofcan  44959  ofmul12  44961  ofdivrec  44962  ofdivcan4  44963  ofdivdiv2  44964  expgrowth  44971  binomcxplemrat  44986  binomcxplemnotnn0  44992  disjf1  45827  dvsinax  46553  dvcosax  46566  dvdivcncf  46567  meadjun  47102  smfmulc1  47436  cjnpoly  47549  f1cof1blem  47734  isubgr0uhgr  48561  uzlidlring  48923  ofaddmndmap  49042  dmatALTbas  49100  dflinc2  49109  fdivmpt  49239  zeroopropdlem  49939  incat  50298  aacllem  50509  amgmwlem  50510