Theorem inidm 4227

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

Syntax hints:   = wceq 1540   ∈ wcel 2108   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958

This theorem is referenced by:  inindi  4235  inindir  4236  uneqin  4289  disjeq0  4456  ssdifeq0  4487  intsng  4983  xpindi  5844  xpindir  5845  resindm  6048  elidinxpid  6063  idinxpresid  6066  predidm  6347  offval2f  7712  fnfvof  7714  ofres  7716  offval2  7717  ofrfval2  7718  coof  7721  ofco  7722  offveq  7723  offveqb  7724  ofc1  7725  ofc2  7726  caofref  7728  caofrss  7736  caoftrn  7738  offsplitfpar  8144  suppssof1  8224  suppofssd  8228  suppofss1d  8229  suppofss2d  8230  fisn  9467  dffi3  9471  ofsubeq0  12263  ofnegsub  12264  ofsubge0  12265  seqof  14100  ofccat  15008  incexc  15873  sadeq  16509  smuval2  16519  smumul  16530  ressinbas  17291  pwsle  17537  pwsleval  17538  mndpsuppss  18778  mndvcl  18810  ghmplusg  19864  gsumzaddlem  19939  gsumzadd  19940  pwspjmhmmgpd  20325  lcomf  20899  crng2idl  21291  frlmipval  21799  frlmphllem  21800  frlmphl  21801  frlmsslsp  21816  frlmup1  21818  psrbaglesupp  21942  psrbagaddcl  21944  psrbagcon  21945  psrbaglefi  21946  psrbagleadd1  21948  psrbagconf1o  21949  gsumbagdiaglem  21950  psraddcl  21958  psraddclOLD  21959  psrvscacl  21971  psrlidm  21982  psrdi  21985  psrdir  21986  psrascl  21999  mplsubglem  22019  psrbagev1  22101  evlslem3  22104  evlslem1  22106  mhpmulcl  22153  psdmplcl  22166  psdadd  22167  psdmul  22170  psdmvr  22173  psrplusgpropd  22237  coe1add  22267  pf1ind  22359  evls1fpws  22373  matplusgcell  22439  matsubgcell  22440  mat1dimscm  22481  baspartn  22961  indistopon  23008  epttop  23016  dissnlocfin  23537  ptbasin  23585  snfil  23872  tsmsadd  24155  ust0  24228  ustuqtop1  24250  rrxcph  25426  rrxds  25427  volun  25580  mbfmulc2lem  25682  mbfaddlem  25695  0pledm  25708  i1faddlem  25728  i1fmullem  25729  i1fadd  25730  i1fmul  25731  itg1addlem4  25734  i1fmulclem  25737  i1fmulc  25738  itg1lea  25747  itg1le  25748  mbfi1fseqlem5  25754  mbfi1flimlem  25757  mbfmullem2  25759  xrge0f  25766  itg2ge0  25770  itg2lea  25779  itg2mulclem  25781  itg2mulc  25782  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2addlem  25793  itg2cnlem1  25796  dvaddf  25979  dvmulf  25980  dvcmulf  25982  dv11cn  26040  plyaddlem1  26252  plyaddlem  26254  coeeulem  26263  coeaddlem  26288  coemulc  26294  dgradd2  26308  dgrcolem2  26314  ofmulrt  26323  plydivlem3  26337  plydivlem4  26338  plydiveu  26340  plyrem  26347  vieta1lem2  26353  elqaalem3  26363  qaa  26365  jensenlem2  27031  jensen  27032  basellem7  27130  basellem9  27132  dchrmulcl  27293  chssoc  31515  chjidm  31539  mdslmd3i  32351  inin  32535  unidifsnne  32554  disjnf  32583  ofrn  32649  ofrn2  32650  ofresid  32652  offinsupp1  32738  gsumle  33101  tocyccntz  33164  elrgspnlem1  33246  islinds5  33395  ellspds  33396  1arithidomlem2  33564  1arithidom  33565  ply1gsumz  33619  ply1degltdimlem  33673  fedgmullem1  33680  hauseqcn  33897  ofcof  34108  carsgclctunlem1  34319  carsgclctun  34323  sibfof  34342  plymul02  34561  signshf  34603  circlemethhgt  34658  msrid  35550  nepss  35718  bj-inrab2  36929  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  broucube  37661  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  ftc1anclem3  37702  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem8  37707  blbnd  37794  lshpinN  38990  lfladdcl  39072  lflvscl  39078  ldualvaddval  39132  lclkrlem2e  41513  ofun  42277  mplmapghm  42566  evlsvvval  42573  fsuppind  42600  fsuppssind  42603  mhphf  42607  mzpclall  42738  mzpindd  42757  dgrsub2  43147  mpaaeu  43162  mendring  43200  ofoafo  43369  ofoacl  43370  ofoaid1  43371  ofoaid2  43372  ofoaass  43373  ofoacom  43374  naddcnff  43375  naddcnffo  43377  naddcnfcom  43379  naddcnfid1  43380  naddcnfass  43382  relexpaddss  43731  ntrkbimka  44051  clsk3nimkb  44053  caofcan  44342  ofmul12  44344  ofdivrec  44345  ofdivcan4  44346  ofdivdiv2  44347  expgrowth  44354  binomcxplemrat  44369  binomcxplemnotnn0  44375  disjf1  45188  dvsinax  45928  dvcosax  45941  dvdivcncf  45942  meadjun  46477  smfmulc1  46811  f1cof1blem  47086  isubgr0uhgr  47859  uzlidlring  48151  ofaddmndmap  48259  dmatALTbas  48318  dflinc2  48327  fdivmpt  48461  aacllem  49320  amgmwlem  49321