Theorem inidm 4179

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146   ∩ cin 3905

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  inindi  4187  inindir  4188  uneqin  4242  disjeq0  4416  ssdifeq0  4449  intsng  4950  xpindi  5821  xpindir  5822  resindmOLD  6032  elidinxpid  6049  idinxpresid  6052  predidm  6331  offval2f  7699  fnfvof  7701  ofres  7703  offval2  7704  ofrfval2  7705  coof  7708  ofco  7709  offveq  7710  offveqb  7711  ofc1  7712  ofc2  7713  caofref  7715  caofrss  7723  caoftrn  7725  offsplitfpar  8120  suppssof1  8201  suppofssd  8205  suppofss1d  8206  suppofss2d  8207  fisn  9394  dffi3  9398  ofsubeq0  12234  ofnegsub  12235  ofsubge0  12236  seqof  14117  ofccat  15034  incexc  15918  sadeq  16556  smuval2  16566  smumul  16577  ressinbas  17331  pwsle  17572  pwsleval  17573  mndpsuppss  18864  mndvcl  18896  ghmplusg  19964  gsumzaddlem  20039  gsumzadd  20040  gsumle  20263  pwspjmhmmgpd  20459  lcomf  21076  crng2idl  21474  frlmipval  21983  frlmphllem  21984  frlmphl  21985  frlmsslsp  22000  frlmup1  22002  psrbaglesupp  22126  psrbagaddcl  22128  psrbagcon  22129  psrbaglefi  22130  psrbagleadd1  22132  psrbagconf1o  22133  gsumbagdiaglem  22135  psraddcl  22143  psrvscacl  22155  psrlidm  22165  psrdi  22168  psrdir  22169  psrascl  22182  mplsubglem  22202  psrbagev1  22282  evlslem3  22285  evlslem1  22287  evlsvvval  22298  mplmapghm  22327  mhpmulcl  22366  psdmplcl  22379  psdadd  22380  psdmul  22383  psdmvr  22386  psrplusgpropd  22449  coe1add  22479  pf1ind  22569  evls1fpws  22583  matplusgcell  22644  matsubgcell  22645  mat1dimscm  22686  baspartn  23165  indistopon  23212  epttop  23220  dissnlocfin  23741  ptbasin  23789  snfil  24076  tsmsadd  24359  ust0  24432  ustuqtop1  24453  rrxcph  25606  rrxds  25607  volun  25759  mbfmulc2lem  25861  mbfaddlem  25874  0pledm  25887  i1faddlem  25907  i1fmullem  25908  i1fadd  25909  i1fmul  25910  itg1addlem4  25913  i1fmulclem  25916  i1fmulc  25917  itg1lea  25926  itg1le  25927  mbfi1fseqlem5  25933  mbfi1flimlem  25936  mbfmullem2  25938  xrge0f  25945  itg2ge0  25949  itg2lea  25958  itg2mulclem  25960  itg2mulc  25961  itg2splitlem  25962  itg2split  25963  itg2monolem1  25964  itg2mono  25967  itg2i1fseqle  25968  itg2i1fseq  25969  itg2addlem  25972  itg2cnlem1  25975  dvaddf  26156  dvmulf  26157  dvcmulf  26159  dv11cn  26215  plyaddlem1  26425  plyaddlem  26427  coeeulem  26436  coeaddlem  26461  coemulc  26467  dgradd2  26480  dgrcolem2  26486  ofmulrt  26495  plymul02  26496  plydivlem3  26511  plydivlem4  26512  plydiveu  26514  plyrem  26521  vieta1lem2  26527  elqaalem3  26537  qaa  26539  jensenlem2  27207  jensen  27208  basellem7  27306  basellem9  27308  dchrmulcl  27468  chssoc  31923  chjidm  31947  mdslmd3i  32759  inin  32937  unidifsnne  32957  disjnf  32990  fnfvor  33029  ofrco  33030  ofrn  33059  ofrn2  33060  ofresid  33062  offinsupp1  33145  tocyccntz  33532  elrgspnlem1  33630  islinds5  33750  ellspds  33751  1arithidomlem2  33894  1arithidom  33895  ply1gsumz  33957  0mplrim  33972  selvply1rhmlemb  33977  selvply1rhmlem4  33981  mplvrpmrhm  34005  esplyind  34033  ply1degltdimlem  34080  fedgmullem1  34087  extdgfialglem2  34151  hauseqcn  34356  ofcof  34565  carsgclctunlem1  34776  carsgclctun  34780  sibfof  34799  signshf  35044  circlemethhgt  35099  msrid  36078  nepss  36251  bj-inrab2  37625  matunitlindflem1  38328  matunitlindflem2  38329  poimirlem1  38333  poimirlem2  38334  poimirlem4  38336  poimirlem6  38338  poimirlem7  38339  poimirlem8  38340  poimirlem10  38342  poimirlem11  38343  poimirlem12  38344  poimirlem16  38348  poimirlem17  38349  poimirlem19  38351  poimirlem20  38352  poimirlem23  38355  poimirlem24  38356  poimirlem25  38357  poimirlem28  38360  poimirlem29  38361  poimirlem30  38362  poimirlem31  38363  poimirlem32  38364  broucube  38366  itg2addnclem  38383  itg2addnclem3  38385  itg2addnc  38386  ftc1anclem3  38407  ftc1anclem5  38409  ftc1anclem6  38410  ftc1anclem8  38412  blbnd  38500  disjimeceqim  39515  lshpinN  39825  lfladdcl  39907  lflvscl  39913  ldualvaddval  39967  lclkrlem2e  42347  ofun  43068  fsuppind  43399  fsuppssind  43402  mhphf  43406  mzpclall  43535  mzpindd  43554  dgrsub2  43939  mpaaeu  43954  mendring  43992  ofoafo  44160  ofoacl  44161  ofoaid1  44162  ofoaid2  44163  ofoaass  44164  ofoacom  44165  naddcnff  44166  naddcnffo  44168  naddcnfcom  44170  naddcnfid1  44171  naddcnfass  44173  relexpaddss  44521  ntrkbimka  44841  clsk3nimkb  44843  caofcan  45110  ofmul12  45112  ofdivrec  45113  ofdivcan4  45114  ofdivdiv2  45115  expgrowth  45122  binomcxplemrat  45137  binomcxplemnotnn0  45143  disjf1  45978  dvsinax  46704  dvcosax  46717  dvdivcncf  46718  meadjun  47253  smfmulc1  47587  cjnpoly  47703  f1cof1blem  47888  isubgr0uhgr  48715  uzlidlring  49076  ofaddmndmap  49199  dmatALTbas  49257  dflinc2  49266  fdivmpt  49396  zeroopropdlem  50096  incat  50455  aacllem  50697  amgmwlem  50726