Theorem inidm 4219

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

Syntax hints:   = wceq 1542   ∈ wcel 2107   ∩ cin 3948

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956

This theorem is referenced by:  inindi  4227  inindir  4228  uneqin  4279  disjeq0  4456  ssdifeq0  4487  intsng  4990  xpindi  5834  xpindir  5835  resindm  6031  elidinxpid  6045  idinxpresid  6048  predidm  6328  offval2f  7685  fnfvof  7687  ofres  7689  offval2  7690  ofrfval2  7691  ofco  7693  offveq  7694  offveqb  7695  ofc1  7696  ofc2  7697  caofref  7699  caofrss  7706  caoftrn  7708  offsplitfpar  8105  suppssof1  8184  suppofssd  8188  suppofss1d  8189  suppofss2d  8190  fisn  9422  dffi3  9426  ofsubeq0  12209  ofnegsub  12210  ofsubge0  12211  seqof  14025  ofccat  14916  incexc  15783  sadeq  16413  smuval2  16423  smumul  16434  ressinbas  17190  pwsle  17438  pwsleval  17439  ghmplusg  19714  gsumzaddlem  19789  gsumzadd  19790  pwspjmhmmgpd  20141  lcomf  20511  crng2idl  20877  frlmipval  21334  frlmphllem  21335  frlmphl  21336  frlmsslsp  21351  frlmup1  21353  psrbaglesupp  21477  psrbaglesuppOLD  21478  psrbagaddcl  21481  psrbagaddclOLD  21482  psrbagcon  21483  psrbagconOLD  21484  psrbaglefi  21485  psrbaglefiOLD  21486  psrbagconf1o  21489  psrbagconf1oOLD  21490  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  psraddcl  21502  psrvscacl  21512  psrlidm  21523  psrdi  21526  psrdir  21527  mplsubglem  21558  psrbagev1  21638  psrbagev1OLD  21639  evlslem3  21643  evlslem1  21645  mhpmulcl  21692  psrplusgpropd  21758  coe1add  21786  pf1ind  21874  mndvcl  21893  matplusgcell  21935  matsubgcell  21936  mat1dimscm  21977  baspartn  22457  indistopon  22504  epttop  22512  dissnlocfin  23033  ptbasin  23081  snfil  23368  tsmsadd  23651  ust0  23724  ustuqtop1  23746  rrxcph  24909  rrxds  24910  volun  25062  mbfmulc2lem  25164  mbfaddlem  25177  0pledm  25190  i1faddlem  25210  i1fmullem  25211  i1fadd  25212  i1fmul  25213  itg1addlem4  25216  itg1addlem4OLD  25217  i1fmulclem  25220  i1fmulc  25221  itg1lea  25230  itg1le  25231  mbfi1fseqlem5  25237  mbfi1flimlem  25240  mbfmullem2  25242  xrge0f  25249  itg2ge0  25253  itg2lea  25262  itg2mulclem  25264  itg2mulc  25265  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2mono  25271  itg2i1fseqle  25272  itg2i1fseq  25273  itg2addlem  25276  itg2cnlem1  25279  dvaddf  25459  dvmulf  25460  dvcmulf  25462  dv11cn  25518  plyaddlem1  25727  plyaddlem  25729  coeeulem  25738  coeaddlem  25763  coemulc  25769  dgradd2  25782  dgrcolem2  25788  ofmulrt  25795  plydivlem3  25808  plydivlem4  25809  plydiveu  25811  plyrem  25818  vieta1lem2  25824  elqaalem3  25834  qaa  25836  jensenlem2  26492  jensen  26493  basellem7  26591  basellem9  26593  dchrmulcl  26752  chssoc  30749  chjidm  30773  mdslmd3i  31585  inin  31753  unidifsnne  31773  disjnf  31801  ofrn  31864  ofrn2  31865  ofresid  31867  offinsupp1  31952  gsumle  32242  tocyccntz  32303  islinds5  32480  ellspds  32481  evls1fpws  32646  ply1gsumz  32669  ply1degltdimlem  32707  fedgmullem1  32714  hauseqcn  32878  ofcof  33105  carsgclctunlem1  33316  carsgclctun  33320  sibfof  33339  plymul02  33557  signshf  33599  circlemethhgt  33655  msrid  34536  nepss  34687  bj-inrab2  35808  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem28  36516  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  broucube  36522  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  ftc1anclem3  36563  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem8  36568  blbnd  36655  lshpinN  37859  lfladdcl  37941  lflvscl  37947  ldualvaddval  38001  lclkrlem2e  40382  ofun  41058  mplmapghm  41128  evlsvvval  41135  fsuppind  41162  fsuppssind  41165  mhphf  41169  mzpclall  41465  mzpindd  41484  dgrsub2  41877  mpaaeu  41892  mendring  41934  ofoafo  42106  ofoacl  42107  ofoaid1  42108  ofoaid2  42109  ofoaass  42110  ofoacom  42111  naddcnff  42112  naddcnffo  42114  naddcnfcom  42116  naddcnfid1  42117  naddcnfass  42119  relexpaddss  42469  ntrkbimka  42789  clsk3nimkb  42791  caofcan  43082  ofmul12  43084  ofdivrec  43085  ofdivcan4  43086  ofdivdiv2  43087  expgrowth  43094  binomcxplemrat  43109  binomcxplemnotnn0  43115  disjf1  43880  dvsinax  44629  dvcosax  44642  dvdivcncf  44643  meadjun  45178  smfmulc1  45512  f1cof1blem  45784  uzlidlring  46827  ofaddmndmap  47019  mndpsuppss  47047  dmatALTbas  47082  dflinc2  47091  fdivmpt  47226  aacllem  47848  amgmwlem  47849