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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2143   ∩ cin 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is used by:  inindi  4187  inindir  4188  uneqin  4242  disjeq0  4416  ssdifeq0  4447  intsng  4948  xpindi  5819  xpindir  5820  resindmOLD  6030  elidinxpid  6047  idinxpresid  6050  predidm  6327  offval2f  7689  fnfvof  7691  ofres  7693  offval2  7694  ofrfval2  7695  coof  7698  ofco  7699  offveq  7700  offveqb  7701  ofc1  7702  ofc2  7703  caofref  7705  caofrss  7713  caoftrn  7715  offsplitfpar  8110  suppssof1  8191  suppofssd  8195  suppofss1d  8196  suppofss2d  8197  fisn  9383  dffi3  9387  ofsubeq0  12219  ofnegsub  12220  ofsubge0  12221  seqof  14100  ofccat  15011  incexc  15896  sadeq  16534  smuval2  16544  smumul  16555  ressinbas  17309  pwsle  17550  pwsleval  17551  mndpsuppss  18827  mndvcl  18859  ghmplusg  19920  gsumzaddlem  19995  gsumzadd  19996  gsumle  20219  pwspjmhmmgpd  20414  lcomf  21031  crng2idl  21429  frlmipval  21938  frlmphllem  21939  frlmphl  21940  frlmsslsp  21955  frlmup1  21957  psrbaglesupp  22081  psrbagaddcl  22083  psrbagcon  22084  psrbaglefi  22085  psrbagleadd1  22087  psrbagconf1o  22088  gsumbagdiaglem  22090  psraddcl  22098  psrvscacl  22110  psrlidm  22120  psrdi  22123  psrdir  22124  psrascl  22137  mplsubglem  22157  psrbagev1  22237  evlslem3  22240  evlslem1  22242  evlsvvval  22253  mplmapghm  22282  mhpmulcl  22321  psdmplcl  22334  psdadd  22335  psdmul  22338  psdmvr  22341  psrplusgpropd  22404  coe1add  22434  pf1ind  22524  evls1fpws  22538  matplusgcell  22599  matsubgcell  22600  mat1dimscm  22641  baspartn  23120  indistopon  23167  epttop  23175  dissnlocfin  23695  ptbasin  23743  snfil  24030  tsmsadd  24313  ust0  24386  ustuqtop1  24407  rrxcph  25560  rrxds  25561  volun  25713  mbfmulc2lem  25815  mbfaddlem  25828  0pledm  25841  i1faddlem  25861  i1fmullem  25862  i1fadd  25863  i1fmul  25864  itg1addlem4  25867  i1fmulclem  25870  i1fmulc  25871  itg1lea  25880  itg1le  25881  mbfi1fseqlem5  25887  mbfi1flimlem  25890  mbfmullem2  25892  xrge0f  25899  itg2ge0  25903  itg2lea  25912  itg2mulclem  25914  itg2mulc  25915  itg2splitlem  25916  itg2split  25917  itg2monolem1  25918  itg2mono  25921  itg2i1fseqle  25922  itg2i1fseq  25923  itg2addlem  25926  itg2cnlem1  25929  dvaddf  26110  dvmulf  26111  dvcmulf  26113  dv11cn  26169  plyaddlem1  26379  plyaddlem  26381  coeeulem  26390  coeaddlem  26415  coemulc  26421  dgradd2  26434  dgrcolem2  26440  ofmulrt  26449  plymul02  26450  plydivlem3  26465  plydivlem4  26466  plydiveu  26468  plyrem  26475  vieta1lem2  26481  elqaalem3  26491  qaa  26493  jensenlem2  27161  jensen  27162  basellem7  27260  basellem9  27262  dchrmulcl  27422  chssoc  31857  chjidm  31881  mdslmd3i  32693  inin  32871  unidifsnne  32891  disjnf  32924  fnfvor  32963  ofrco  32964  ofrn  32993  ofrn2  32994  ofresid  32996  offinsupp1  33080  tocyccntz  33473  elrgspnlem1  33571  islinds5  33691  ellspds  33692  1arithidomlem2  33835  1arithidom  33836  ply1gsumz  33898  0mplrim  33913  selvply1rhmlemb  33918  selvply1rhmlem4  33922  mplvrpmrhm  33946  esplyind  33974  ply1degltdimlem  34021  fedgmullem1  34028  extdgfialglem2  34092  hauseqcn  34297  ofcof  34506  carsgclctunlem1  34716  carsgclctun  34720  sibfof  34739  signshf  34984  circlemethhgt  35039  msrid  36045  nepss  36218  bj-inrab2  37592  matunitlindflem1  38295  matunitlindflem2  38296  poimirlem1  38300  poimirlem2  38301  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem28  38327  poimirlem29  38328  poimirlem30  38329  poimirlem31  38330  poimirlem32  38331  broucube  38333  itg2addnclem  38350  itg2addnclem3  38352  itg2addnc  38353  ftc1anclem3  38374  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem8  38379  blbnd  38466  disjimeceqim  39481  lshpinN  39791  lfladdcl  39873  lflvscl  39879  ldualvaddval  39933  lclkrlem2e  42313  ofun  43034  fsuppind  43350  fsuppssind  43353  mhphf  43357  mzpclall  43486  mzpindd  43505  dgrsub2  43890  mpaaeu  43905  mendring  43943  ofoafo  44111  ofoacl  44112  ofoaid1  44113  ofoaid2  44114  ofoaass  44115  ofoacom  44116  naddcnff  44117  naddcnffo  44119  naddcnfcom  44121  naddcnfid1  44122  naddcnfass  44124  relexpaddss  44472  ntrkbimka  44792  clsk3nimkb  44794  caofcan  45061  ofmul12  45063  ofdivrec  45064  ofdivcan4  45065  ofdivdiv2  45066  expgrowth  45073  binomcxplemrat  45088  binomcxplemnotnn0  45094  disjf1  45929  dvsinax  46655  dvcosax  46668  dvdivcncf  46669  meadjun  47204  smfmulc1  47538  cjnpoly  47654  f1cof1blem  47839  isubgr0uhgr  48666  uzlidlring  49028  ofaddmndmap  49151  dmatALTbas  49209  dflinc2  49218  fdivmpt  49348  zeroopropdlem  50048  incat  50407  aacllem  50649  amgmwlem  50677