Theorem inidm 4181

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

Syntax hints:   = wceq 1542   ∈ wcel 2114   ∩ cin 3902

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910

This theorem is referenced by:  inindi  4189  inindir  4190  uneqin  4243  disjeq0  4410  ssdifeq0  4441  intsng  4940  xpindi  5792  xpindir  5793  resindm  5999  elidinxpid  6014  idinxpresid  6017  predidm  6294  offval2f  7649  fnfvof  7651  ofres  7653  offval2  7654  ofrfval2  7655  coof  7658  ofco  7659  offveq  7660  offveqb  7661  ofc1  7662  ofc2  7663  caofref  7665  caofrss  7673  caoftrn  7675  offsplitfpar  8073  suppssof1  8153  suppofssd  8157  suppofss1d  8158  suppofss2d  8159  fisn  9344  dffi3  9348  ofsubeq0  12156  ofnegsub  12157  ofsubge0  12158  seqof  13996  ofccat  14906  incexc  15774  sadeq  16413  smuval2  16423  smumul  16434  ressinbas  17186  pwsle  17427  pwsleval  17428  mndpsuppss  18704  mndvcl  18736  ghmplusg  19792  gsumzaddlem  19867  gsumzadd  19868  gsumle  20091  pwspjmhmmgpd  20280  lcomf  20869  crng2idl  21253  frlmipval  21751  frlmphllem  21752  frlmphl  21753  frlmsslsp  21768  frlmup1  21770  psrbaglesupp  21895  psrbagaddcl  21897  psrbagcon  21898  psrbaglefi  21899  psrbagleadd1  21901  psrbagconf1o  21902  gsumbagdiaglem  21903  psraddcl  21911  psraddclOLD  21912  psrvscacl  21924  psrlidm  21934  psrdi  21937  psrdir  21938  psrascl  21951  mplsubglem  21971  psrbagev1  22049  evlslem3  22052  evlslem1  22054  evlsvvval  22065  mhpmulcl  22109  psdmplcl  22122  psdadd  22123  psdmul  22126  psdmvr  22129  psrplusgpropd  22193  coe1add  22223  pf1ind  22316  evls1fpws  22330  matplusgcell  22394  matsubgcell  22395  mat1dimscm  22436  baspartn  22915  indistopon  22962  epttop  22970  dissnlocfin  23490  ptbasin  23538  snfil  23825  tsmsadd  24108  ust0  24181  ustuqtop1  24202  rrxcph  25365  rrxds  25366  volun  25519  mbfmulc2lem  25621  mbfaddlem  25634  0pledm  25647  i1faddlem  25667  i1fmullem  25668  i1fadd  25669  i1fmul  25670  itg1addlem4  25673  i1fmulclem  25676  i1fmulc  25677  itg1lea  25686  itg1le  25687  mbfi1fseqlem5  25693  mbfi1flimlem  25696  mbfmullem2  25698  xrge0f  25705  itg2ge0  25709  itg2lea  25718  itg2mulclem  25720  itg2mulc  25721  itg2splitlem  25722  itg2split  25723  itg2monolem1  25724  itg2mono  25727  itg2i1fseqle  25728  itg2i1fseq  25729  itg2addlem  25732  itg2cnlem1  25735  dvaddf  25918  dvmulf  25919  dvcmulf  25921  dv11cn  25979  plyaddlem1  26191  plyaddlem  26193  coeeulem  26202  coeaddlem  26227  coemulc  26233  dgradd2  26247  dgrcolem2  26253  ofmulrt  26262  plydivlem3  26276  plydivlem4  26277  plydiveu  26279  plyrem  26286  vieta1lem2  26292  elqaalem3  26302  qaa  26304  jensenlem2  26971  jensen  26972  basellem7  27070  basellem9  27072  dchrmulcl  27233  chssoc  31590  chjidm  31614  mdslmd3i  32426  inin  32609  unidifsnne  32629  disjnf  32663  fnfvor  32705  ofrco  32706  ofrn  32735  ofrn2  32736  ofresid  32738  offinsupp1  32822  tocyccntz  33244  elrgspnlem1  33342  islinds5  33466  ellspds  33467  1arithidomlem2  33635  1arithidom  33636  ply1gsumz  33698  mplvrpmrhm  33730  esplyind  33758  ply1degltdimlem  33806  fedgmullem1  33813  extdgfialglem2  33877  hauseqcn  34082  ofcof  34291  carsgclctunlem1  34501  carsgclctun  34505  sibfof  34524  plymul02  34730  signshf  34772  circlemethhgt  34827  msrid  35767  nepss  35940  bj-inrab2  37203  matunitlindflem1  37896  matunitlindflem2  37897  poimirlem1  37901  poimirlem2  37902  poimirlem3  37903  poimirlem4  37904  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  poimirlem10  37910  poimirlem11  37911  poimirlem12  37912  poimirlem16  37916  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem23  37923  poimirlem24  37924  poimirlem25  37925  poimirlem28  37928  poimirlem29  37929  poimirlem30  37930  poimirlem31  37931  poimirlem32  37932  broucube  37934  itg2addnclem  37951  itg2addnclem3  37953  itg2addnc  37954  ftc1anclem3  37975  ftc1anclem5  37977  ftc1anclem6  37978  ftc1anclem8  37980  blbnd  38067  disjimeceqim  39084  lshpinN  39394  lfladdcl  39476  lflvscl  39482  ldualvaddval  39536  lclkrlem2e  41916  ofun  42637  mplmapghm  42951  fsuppind  42977  fsuppssind  42980  mhphf  42984  mzpclall  43113  mzpindd  43132  dgrsub2  43521  mpaaeu  43536  mendring  43574  ofoafo  43742  ofoacl  43743  ofoaid1  43744  ofoaid2  43745  ofoaass  43746  ofoacom  43747  naddcnff  43748  naddcnffo  43750  naddcnfcom  43752  naddcnfid1  43753  naddcnfass  43755  relexpaddss  44103  ntrkbimka  44423  clsk3nimkb  44425  caofcan  44708  ofmul12  44710  ofdivrec  44711  ofdivcan4  44712  ofdivdiv2  44713  expgrowth  44720  binomcxplemrat  44735  binomcxplemnotnn0  44741  disjf1  45571  dvsinax  46300  dvcosax  46313  dvdivcncf  46314  meadjun  46849  smfmulc1  47183  cjnpoly  47278  f1cof1blem  47463  isubgr0uhgr  48262  uzlidlring  48624  ofaddmndmap  48732  dmatALTbas  48790  dflinc2  48799  fdivmpt  48929  zeroopropdlem  49630  incat  49989  aacllem  50189  amgmwlem  50190