Theorem inidm 4186

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

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

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 3446  df-in 3918

This theorem is referenced by:  inindi  4194  inindir  4195  uneqin  4248  disjeq0  4415  ssdifeq0  4446  intsng  4943  xpindi  5787  xpindir  5788  resindm  5990  elidinxpid  6005  idinxpresid  6008  predidm  6287  offval2f  7648  fnfvof  7650  ofres  7652  offval2  7653  ofrfval2  7654  coof  7657  ofco  7658  offveq  7659  offveqb  7660  ofc1  7661  ofc2  7662  caofref  7664  caofrss  7672  caoftrn  7674  offsplitfpar  8075  suppssof1  8155  suppofssd  8159  suppofss1d  8160  suppofss2d  8161  fisn  9354  dffi3  9358  ofsubeq0  12159  ofnegsub  12160  ofsubge0  12161  seqof  14000  ofccat  14911  incexc  15779  sadeq  16418  smuval2  16428  smumul  16439  ressinbas  17191  pwsle  17431  pwsleval  17432  mndpsuppss  18674  mndvcl  18706  ghmplusg  19760  gsumzaddlem  19835  gsumzadd  19836  gsumle  20059  pwspjmhmmgpd  20248  lcomf  20839  crng2idl  21223  frlmipval  21721  frlmphllem  21722  frlmphl  21723  frlmsslsp  21738  frlmup1  21740  psrbaglesupp  21864  psrbagaddcl  21866  psrbagcon  21867  psrbaglefi  21868  psrbagleadd1  21870  psrbagconf1o  21871  gsumbagdiaglem  21872  psraddcl  21880  psraddclOLD  21881  psrvscacl  21893  psrlidm  21904  psrdi  21907  psrdir  21908  psrascl  21921  mplsubglem  21941  psrbagev1  22017  evlslem3  22020  evlslem1  22022  mhpmulcl  22069  psdmplcl  22082  psdadd  22083  psdmul  22086  psdmvr  22089  psrplusgpropd  22153  coe1add  22183  pf1ind  22275  evls1fpws  22289  matplusgcell  22353  matsubgcell  22354  mat1dimscm  22395  baspartn  22874  indistopon  22921  epttop  22929  dissnlocfin  23449  ptbasin  23497  snfil  23784  tsmsadd  24067  ust0  24140  ustuqtop1  24162  rrxcph  25325  rrxds  25326  volun  25479  mbfmulc2lem  25581  mbfaddlem  25594  0pledm  25607  i1faddlem  25627  i1fmullem  25628  i1fadd  25629  i1fmul  25630  itg1addlem4  25633  i1fmulclem  25636  i1fmulc  25637  itg1lea  25646  itg1le  25647  mbfi1fseqlem5  25653  mbfi1flimlem  25656  mbfmullem2  25658  xrge0f  25665  itg2ge0  25669  itg2lea  25678  itg2mulclem  25680  itg2mulc  25681  itg2splitlem  25682  itg2split  25683  itg2monolem1  25684  itg2mono  25687  itg2i1fseqle  25688  itg2i1fseq  25689  itg2addlem  25692  itg2cnlem1  25695  dvaddf  25878  dvmulf  25879  dvcmulf  25881  dv11cn  25939  plyaddlem1  26151  plyaddlem  26153  coeeulem  26162  coeaddlem  26187  coemulc  26193  dgradd2  26207  dgrcolem2  26213  ofmulrt  26222  plydivlem3  26236  plydivlem4  26237  plydiveu  26239  plyrem  26246  vieta1lem2  26252  elqaalem3  26262  qaa  26264  jensenlem2  26931  jensen  26932  basellem7  27030  basellem9  27032  dchrmulcl  27193  chssoc  31475  chjidm  31499  mdslmd3i  32311  inin  32495  unidifsnne  32515  disjnf  32549  ofrn  32613  ofrn2  32614  ofresid  32616  offinsupp1  32700  tocyccntz  33116  elrgspnlem1  33209  islinds5  33331  ellspds  33332  1arithidomlem2  33500  1arithidom  33501  ply1gsumz  33557  ply1degltdimlem  33611  fedgmullem1  33618  hauseqcn  33881  ofcof  34090  carsgclctunlem1  34301  carsgclctun  34305  sibfof  34324  plymul02  34530  signshf  34572  circlemethhgt  34627  msrid  35525  nepss  35698  bj-inrab2  36909  matunitlindflem1  37603  matunitlindflem2  37604  poimirlem1  37608  poimirlem2  37609  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem28  37635  poimirlem29  37636  poimirlem30  37637  poimirlem31  37638  poimirlem32  37639  broucube  37641  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  ftc1anclem3  37682  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem8  37687  blbnd  37774  lshpinN  38975  lfladdcl  39057  lflvscl  39063  ldualvaddval  39117  lclkrlem2e  41498  ofun  42217  mplmapghm  42537  evlsvvval  42544  fsuppind  42571  fsuppssind  42574  mhphf  42578  mzpclall  42708  mzpindd  42727  dgrsub2  43117  mpaaeu  43132  mendring  43170  ofoafo  43338  ofoacl  43339  ofoaid1  43340  ofoaid2  43341  ofoaass  43342  ofoacom  43343  naddcnff  43344  naddcnffo  43346  naddcnfcom  43348  naddcnfid1  43349  naddcnfass  43351  relexpaddss  43700  ntrkbimka  44020  clsk3nimkb  44022  caofcan  44305  ofmul12  44307  ofdivrec  44308  ofdivcan4  44309  ofdivdiv2  44310  expgrowth  44317  binomcxplemrat  44332  binomcxplemnotnn0  44338  disjf1  45170  dvsinax  45904  dvcosax  45917  dvdivcncf  45918  meadjun  46453  smfmulc1  46787  cjnpoly  46883  f1cof1blem  47068  isubgr0uhgr  47866  uzlidlring  48216  ofaddmndmap  48324  dmatALTbas  48383  dflinc2  48392  fdivmpt  48522  zeroopropdlem  49224  incat  49583  aacllem  49783  amgmwlem  49784