Theorem inidm 4190

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

Syntax hints:   = wceq 1540   ∈ wcel 2109   ∩ cin 3913

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  inindi  4198  inindir  4199  uneqin  4252  disjeq0  4419  ssdifeq0  4450  intsng  4947  xpindi  5797  xpindir  5798  resindm  6001  elidinxpid  6016  idinxpresid  6019  predidm  6299  offval2f  7668  fnfvof  7670  ofres  7672  offval2  7673  ofrfval2  7674  coof  7677  ofco  7678  offveq  7679  offveqb  7680  ofc1  7681  ofc2  7682  caofref  7684  caofrss  7692  caoftrn  7694  offsplitfpar  8098  suppssof1  8178  suppofssd  8182  suppofss1d  8183  suppofss2d  8184  fisn  9378  dffi3  9382  ofsubeq0  12183  ofnegsub  12184  ofsubge0  12185  seqof  14024  ofccat  14935  incexc  15803  sadeq  16442  smuval2  16452  smumul  16463  ressinbas  17215  pwsle  17455  pwsleval  17456  mndpsuppss  18692  mndvcl  18724  ghmplusg  19776  gsumzaddlem  19851  gsumzadd  19852  pwspjmhmmgpd  20237  lcomf  20807  crng2idl  21191  frlmipval  21688  frlmphllem  21689  frlmphl  21690  frlmsslsp  21705  frlmup1  21707  psrbaglesupp  21831  psrbagaddcl  21833  psrbagcon  21834  psrbaglefi  21835  psrbagleadd1  21837  psrbagconf1o  21838  gsumbagdiaglem  21839  psraddcl  21847  psraddclOLD  21848  psrvscacl  21860  psrlidm  21871  psrdi  21874  psrdir  21875  psrascl  21888  mplsubglem  21908  psrbagev1  21984  evlslem3  21987  evlslem1  21989  mhpmulcl  22036  psdmplcl  22049  psdadd  22050  psdmul  22053  psdmvr  22056  psrplusgpropd  22120  coe1add  22150  pf1ind  22242  evls1fpws  22256  matplusgcell  22320  matsubgcell  22321  mat1dimscm  22362  baspartn  22841  indistopon  22888  epttop  22896  dissnlocfin  23416  ptbasin  23464  snfil  23751  tsmsadd  24034  ust0  24107  ustuqtop1  24129  rrxcph  25292  rrxds  25293  volun  25446  mbfmulc2lem  25548  mbfaddlem  25561  0pledm  25574  i1faddlem  25594  i1fmullem  25595  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  i1fmulclem  25603  i1fmulc  25604  itg1lea  25613  itg1le  25614  mbfi1fseqlem5  25620  mbfi1flimlem  25623  mbfmullem2  25625  xrge0f  25632  itg2ge0  25636  itg2lea  25645  itg2mulclem  25647  itg2mulc  25648  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2mono  25654  itg2i1fseqle  25655  itg2i1fseq  25656  itg2addlem  25659  itg2cnlem1  25662  dvaddf  25845  dvmulf  25846  dvcmulf  25848  dv11cn  25906  plyaddlem1  26118  plyaddlem  26120  coeeulem  26129  coeaddlem  26154  coemulc  26160  dgradd2  26174  dgrcolem2  26180  ofmulrt  26189  plydivlem3  26203  plydivlem4  26204  plydiveu  26206  plyrem  26213  vieta1lem2  26219  elqaalem3  26229  qaa  26231  jensenlem2  26898  jensen  26899  basellem7  26997  basellem9  26999  dchrmulcl  27160  chssoc  31425  chjidm  31449  mdslmd3i  32261  inin  32445  unidifsnne  32465  disjnf  32499  ofrn  32563  ofrn2  32564  ofresid  32566  offinsupp1  32650  gsumle  33038  tocyccntz  33101  elrgspnlem1  33193  islinds5  33338  ellspds  33339  1arithidomlem2  33507  1arithidom  33508  ply1gsumz  33564  ply1degltdimlem  33618  fedgmullem1  33625  hauseqcn  33888  ofcof  34097  carsgclctunlem1  34308  carsgclctun  34312  sibfof  34331  plymul02  34537  signshf  34579  circlemethhgt  34634  msrid  35532  nepss  35705  bj-inrab2  36916  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  broucube  37648  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem3  37689  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem8  37694  blbnd  37781  lshpinN  38982  lfladdcl  39064  lflvscl  39070  ldualvaddval  39124  lclkrlem2e  41505  ofun  42224  mplmapghm  42544  evlsvvval  42551  fsuppind  42578  fsuppssind  42581  mhphf  42585  mzpclall  42715  mzpindd  42734  dgrsub2  43124  mpaaeu  43139  mendring  43177  ofoafo  43345  ofoacl  43346  ofoaid1  43347  ofoaid2  43348  ofoaass  43349  ofoacom  43350  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfass  43358  relexpaddss  43707  ntrkbimka  44027  clsk3nimkb  44029  caofcan  44312  ofmul12  44314  ofdivrec  44315  ofdivcan4  44316  ofdivdiv2  44317  expgrowth  44324  binomcxplemrat  44339  binomcxplemnotnn0  44345  disjf1  45177  dvsinax  45911  dvcosax  45924  dvdivcncf  45925  meadjun  46460  smfmulc1  46794  cjnpoly  46890  f1cof1blem  47075  isubgr0uhgr  47873  uzlidlring  48223  ofaddmndmap  48331  dmatALTbas  48390  dflinc2  48399  fdivmpt  48529  zeroopropdlem  49231  incat  49590  aacllem  49790  amgmwlem  49791