Theorem inidm 4180

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

Syntax hints:   = wceq 1542   ∈ wcel 2114   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-in 3909

This theorem is referenced by:  inindi  4188  inindir  4189  uneqin  4242  disjeq0  4409  ssdifeq0  4440  intsng  4939  xpindi  5783  xpindir  5784  resindm  5990  elidinxpid  6005  idinxpresid  6008  predidm  6285  offval2f  7639  fnfvof  7641  ofres  7643  offval2  7644  ofrfval2  7645  coof  7648  ofco  7649  offveq  7650  offveqb  7651  ofc1  7652  ofc2  7653  caofref  7655  caofrss  7663  caoftrn  7665  offsplitfpar  8063  suppssof1  8143  suppofssd  8147  suppofss1d  8148  suppofss2d  8149  fisn  9334  dffi3  9338  ofsubeq0  12146  ofnegsub  12147  ofsubge0  12148  seqof  13986  ofccat  14896  incexc  15764  sadeq  16403  smuval2  16413  smumul  16424  ressinbas  17176  pwsle  17417  pwsleval  17418  mndpsuppss  18694  mndvcl  18726  ghmplusg  19779  gsumzaddlem  19854  gsumzadd  19855  gsumle  20078  pwspjmhmmgpd  20267  lcomf  20856  crng2idl  21240  frlmipval  21738  frlmphllem  21739  frlmphl  21740  frlmsslsp  21755  frlmup1  21757  psrbaglesupp  21882  psrbagaddcl  21884  psrbagcon  21885  psrbaglefi  21886  psrbagleadd1  21888  psrbagconf1o  21889  gsumbagdiaglem  21890  psraddcl  21898  psraddclOLD  21899  psrvscacl  21911  psrlidm  21921  psrdi  21924  psrdir  21925  psrascl  21938  mplsubglem  21958  psrbagev1  22036  evlslem3  22039  evlslem1  22041  evlsvvval  22052  mhpmulcl  22096  psdmplcl  22109  psdadd  22110  psdmul  22113  psdmvr  22116  psrplusgpropd  22180  coe1add  22210  pf1ind  22303  evls1fpws  22317  matplusgcell  22381  matsubgcell  22382  mat1dimscm  22423  baspartn  22902  indistopon  22949  epttop  22957  dissnlocfin  23477  ptbasin  23525  snfil  23812  tsmsadd  24095  ust0  24168  ustuqtop1  24189  rrxcph  25352  rrxds  25353  volun  25506  mbfmulc2lem  25608  mbfaddlem  25621  0pledm  25634  i1faddlem  25654  i1fmullem  25655  i1fadd  25656  i1fmul  25657  itg1addlem4  25660  i1fmulclem  25663  i1fmulc  25664  itg1lea  25673  itg1le  25674  mbfi1fseqlem5  25680  mbfi1flimlem  25683  mbfmullem2  25685  xrge0f  25692  itg2ge0  25696  itg2lea  25705  itg2mulclem  25707  itg2mulc  25708  itg2splitlem  25709  itg2split  25710  itg2monolem1  25711  itg2mono  25714  itg2i1fseqle  25715  itg2i1fseq  25716  itg2addlem  25719  itg2cnlem1  25722  dvaddf  25905  dvmulf  25906  dvcmulf  25908  dv11cn  25966  plyaddlem1  26178  plyaddlem  26180  coeeulem  26189  coeaddlem  26214  coemulc  26220  dgradd2  26234  dgrcolem2  26240  ofmulrt  26249  plydivlem3  26263  plydivlem4  26264  plydiveu  26266  plyrem  26273  vieta1lem2  26279  elqaalem3  26289  qaa  26291  jensenlem2  26958  jensen  26959  basellem7  27057  basellem9  27059  dchrmulcl  27220  chssoc  31575  chjidm  31599  mdslmd3i  32411  inin  32594  unidifsnne  32614  disjnf  32648  fnfvor  32690  ofrco  32691  ofrn  32720  ofrn2  32721  ofresid  32723  offinsupp1  32807  tocyccntz  33228  elrgspnlem1  33326  islinds5  33450  ellspds  33451  1arithidomlem2  33619  1arithidom  33620  ply1gsumz  33682  mplvrpmrhm  33714  esplyind  33733  ply1degltdimlem  33781  fedgmullem1  33788  extdgfialglem2  33852  hauseqcn  34057  ofcof  34266  carsgclctunlem1  34476  carsgclctun  34480  sibfof  34499  plymul02  34705  signshf  34747  circlemethhgt  34802  msrid  35741  nepss  35914  bj-inrab2  37131  matunitlindflem1  37819  matunitlindflem2  37820  poimirlem1  37824  poimirlem2  37825  poimirlem3  37826  poimirlem4  37827  poimirlem6  37829  poimirlem7  37830  poimirlem8  37831  poimirlem10  37833  poimirlem11  37834  poimirlem12  37835  poimirlem16  37839  poimirlem17  37840  poimirlem19  37842  poimirlem20  37843  poimirlem23  37846  poimirlem24  37847  poimirlem25  37848  poimirlem28  37851  poimirlem29  37852  poimirlem30  37853  poimirlem31  37854  poimirlem32  37855  broucube  37857  itg2addnclem  37874  itg2addnclem3  37876  itg2addnc  37877  ftc1anclem3  37898  ftc1anclem5  37900  ftc1anclem6  37901  ftc1anclem8  37903  blbnd  37990  disjimeceqim  39007  lshpinN  39317  lfladdcl  39399  lflvscl  39405  ldualvaddval  39459  lclkrlem2e  41839  ofun  42560  mplmapghm  42874  fsuppind  42900  fsuppssind  42903  mhphf  42907  mzpclall  43036  mzpindd  43055  dgrsub2  43444  mpaaeu  43459  mendring  43497  ofoafo  43665  ofoacl  43666  ofoaid1  43667  ofoaid2  43668  ofoaass  43669  ofoacom  43670  naddcnff  43671  naddcnffo  43673  naddcnfcom  43675  naddcnfid1  43676  naddcnfass  43678  relexpaddss  44026  ntrkbimka  44346  clsk3nimkb  44348  caofcan  44631  ofmul12  44633  ofdivrec  44634  ofdivcan4  44635  ofdivdiv2  44636  expgrowth  44643  binomcxplemrat  44658  binomcxplemnotnn0  44664  disjf1  45494  dvsinax  46224  dvcosax  46237  dvdivcncf  46238  meadjun  46773  smfmulc1  47107  cjnpoly  47202  f1cof1blem  47387  isubgr0uhgr  48186  uzlidlring  48548  ofaddmndmap  48656  dmatALTbas  48714  dflinc2  48723  fdivmpt  48853  zeroopropdlem  49554  incat  49913  aacllem  50113  amgmwlem  50114