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

Syntax hints:   = wceq 1541   ∈ wcel 2113   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  inindi  4187  inindir  4188  uneqin  4241  disjeq0  4408  ssdifeq0  4439  intsng  4938  xpindi  5782  xpindir  5783  resindm  5989  elidinxpid  6004  idinxpresid  6007  predidm  6284  offval2f  7637  fnfvof  7639  ofres  7641  offval2  7642  ofrfval2  7643  coof  7646  ofco  7647  offveq  7648  offveqb  7649  ofc1  7650  ofc2  7651  caofref  7653  caofrss  7661  caoftrn  7663  offsplitfpar  8061  suppssof1  8141  suppofssd  8145  suppofss1d  8146  suppofss2d  8147  fisn  9330  dffi3  9334  ofsubeq0  12142  ofnegsub  12143  ofsubge0  12144  seqof  13982  ofccat  14892  incexc  15760  sadeq  16399  smuval2  16409  smumul  16420  ressinbas  17172  pwsle  17413  pwsleval  17414  mndpsuppss  18690  mndvcl  18722  ghmplusg  19775  gsumzaddlem  19850  gsumzadd  19851  gsumle  20074  pwspjmhmmgpd  20263  lcomf  20852  crng2idl  21236  frlmipval  21734  frlmphllem  21735  frlmphl  21736  frlmsslsp  21751  frlmup1  21753  psrbaglesupp  21878  psrbagaddcl  21880  psrbagcon  21881  psrbaglefi  21882  psrbagleadd1  21884  psrbagconf1o  21885  gsumbagdiaglem  21886  psraddcl  21894  psraddclOLD  21895  psrvscacl  21907  psrlidm  21917  psrdi  21920  psrdir  21921  psrascl  21934  mplsubglem  21954  psrbagev1  22032  evlslem3  22035  evlslem1  22037  evlsvvval  22048  mhpmulcl  22092  psdmplcl  22105  psdadd  22106  psdmul  22109  psdmvr  22112  psrplusgpropd  22176  coe1add  22206  pf1ind  22299  evls1fpws  22313  matplusgcell  22377  matsubgcell  22378  mat1dimscm  22419  baspartn  22898  indistopon  22945  epttop  22953  dissnlocfin  23473  ptbasin  23521  snfil  23808  tsmsadd  24091  ust0  24164  ustuqtop1  24185  rrxcph  25348  rrxds  25349  volun  25502  mbfmulc2lem  25604  mbfaddlem  25617  0pledm  25630  i1faddlem  25650  i1fmullem  25651  i1fadd  25652  i1fmul  25653  itg1addlem4  25656  i1fmulclem  25659  i1fmulc  25660  itg1lea  25669  itg1le  25670  mbfi1fseqlem5  25676  mbfi1flimlem  25679  mbfmullem2  25681  xrge0f  25688  itg2ge0  25692  itg2lea  25701  itg2mulclem  25703  itg2mulc  25704  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2addlem  25715  itg2cnlem1  25718  dvaddf  25901  dvmulf  25902  dvcmulf  25904  dv11cn  25962  plyaddlem1  26174  plyaddlem  26176  coeeulem  26185  coeaddlem  26210  coemulc  26216  dgradd2  26230  dgrcolem2  26236  ofmulrt  26245  plydivlem3  26259  plydivlem4  26260  plydiveu  26262  plyrem  26269  vieta1lem2  26275  elqaalem3  26285  qaa  26287  jensenlem2  26954  jensen  26955  basellem7  27053  basellem9  27055  dchrmulcl  27216  chssoc  31571  chjidm  31595  mdslmd3i  32407  inin  32591  unidifsnne  32611  disjnf  32645  fnfvor  32687  ofrco  32688  ofrn  32717  ofrn2  32718  ofresid  32720  offinsupp1  32805  tocyccntz  33226  elrgspnlem1  33324  islinds5  33448  ellspds  33449  1arithidomlem2  33617  1arithidom  33618  ply1gsumz  33680  mplvrpmrhm  33712  esplyind  33731  ply1degltdimlem  33779  fedgmullem1  33786  extdgfialglem2  33850  hauseqcn  34055  ofcof  34264  carsgclctunlem1  34474  carsgclctun  34478  sibfof  34497  plymul02  34703  signshf  34745  circlemethhgt  34800  msrid  35739  nepss  35912  bj-inrab2  37129  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem28  37849  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  broucube  37855  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  ftc1anclem3  37896  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem8  37901  blbnd  37988  lshpinN  39249  lfladdcl  39331  lflvscl  39337  ldualvaddval  39391  lclkrlem2e  41771  ofun  42492  mplmapghm  42807  fsuppind  42833  fsuppssind  42836  mhphf  42840  mzpclall  42969  mzpindd  42988  dgrsub2  43377  mpaaeu  43392  mendring  43430  ofoafo  43598  ofoacl  43599  ofoaid1  43600  ofoaid2  43601  ofoaass  43602  ofoacom  43603  naddcnff  43604  naddcnffo  43606  naddcnfcom  43608  naddcnfid1  43609  naddcnfass  43611  relexpaddss  43959  ntrkbimka  44279  clsk3nimkb  44281  caofcan  44564  ofmul12  44566  ofdivrec  44567  ofdivcan4  44568  ofdivdiv2  44569  expgrowth  44576  binomcxplemrat  44591  binomcxplemnotnn0  44597  disjf1  45427  dvsinax  46157  dvcosax  46170  dvdivcncf  46171  meadjun  46706  smfmulc1  47040  cjnpoly  47135  f1cof1blem  47320  isubgr0uhgr  48119  uzlidlring  48481  ofaddmndmap  48589  dmatALTbas  48647  dflinc2  48656  fdivmpt  48786  zeroopropdlem  49487  incat  49846  aacllem  50046  amgmwlem  50047