Theorem inidm 4177

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906

This theorem is referenced by:  inindi  4185  inindir  4186  uneqin  4239  disjeq0  4406  ssdifeq0  4437  intsng  4936  xpindi  5780  xpindir  5781  resindm  5987  elidinxpid  6002  idinxpresid  6005  predidm  6282  offval2f  7635  fnfvof  7637  ofres  7639  offval2  7640  ofrfval2  7641  coof  7644  ofco  7645  offveq  7646  offveqb  7647  ofc1  7648  ofc2  7649  caofref  7651  caofrss  7659  caoftrn  7661  offsplitfpar  8059  suppssof1  8139  suppofssd  8143  suppofss1d  8144  suppofss2d  8145  fisn  9328  dffi3  9332  ofsubeq0  12140  ofnegsub  12141  ofsubge0  12142  seqof  13980  ofccat  14890  incexc  15758  sadeq  16397  smuval2  16407  smumul  16418  ressinbas  17170  pwsle  17411  pwsleval  17412  mndpsuppss  18688  mndvcl  18720  ghmplusg  19773  gsumzaddlem  19848  gsumzadd  19849  gsumle  20072  pwspjmhmmgpd  20261  lcomf  20850  crng2idl  21234  frlmipval  21732  frlmphllem  21733  frlmphl  21734  frlmsslsp  21749  frlmup1  21751  psrbaglesupp  21876  psrbagaddcl  21878  psrbagcon  21879  psrbaglefi  21880  psrbagleadd1  21882  psrbagconf1o  21883  gsumbagdiaglem  21884  psraddcl  21892  psraddclOLD  21893  psrvscacl  21905  psrlidm  21915  psrdi  21918  psrdir  21919  psrascl  21932  mplsubglem  21952  psrbagev1  22030  evlslem3  22033  evlslem1  22035  evlsvvval  22046  mhpmulcl  22090  psdmplcl  22103  psdadd  22104  psdmul  22107  psdmvr  22110  psrplusgpropd  22174  coe1add  22204  pf1ind  22297  evls1fpws  22311  matplusgcell  22375  matsubgcell  22376  mat1dimscm  22417  baspartn  22896  indistopon  22943  epttop  22951  dissnlocfin  23471  ptbasin  23519  snfil  23806  tsmsadd  24089  ust0  24162  ustuqtop1  24183  rrxcph  25346  rrxds  25347  volun  25500  mbfmulc2lem  25602  mbfaddlem  25615  0pledm  25628  i1faddlem  25648  i1fmullem  25649  i1fadd  25650  i1fmul  25651  itg1addlem4  25654  i1fmulclem  25657  i1fmulc  25658  itg1lea  25667  itg1le  25668  mbfi1fseqlem5  25674  mbfi1flimlem  25677  mbfmullem2  25679  xrge0f  25686  itg2ge0  25690  itg2lea  25699  itg2mulclem  25701  itg2mulc  25702  itg2splitlem  25703  itg2split  25704  itg2monolem1  25705  itg2mono  25708  itg2i1fseqle  25709  itg2i1fseq  25710  itg2addlem  25713  itg2cnlem1  25716  dvaddf  25899  dvmulf  25900  dvcmulf  25902  dv11cn  25960  plyaddlem1  26172  plyaddlem  26174  coeeulem  26183  coeaddlem  26208  coemulc  26214  dgradd2  26228  dgrcolem2  26234  ofmulrt  26243  plydivlem3  26257  plydivlem4  26258  plydiveu  26260  plyrem  26267  vieta1lem2  26273  elqaalem3  26283  qaa  26285  jensenlem2  26952  jensen  26953  basellem7  27051  basellem9  27053  dchrmulcl  27214  chssoc  31520  chjidm  31544  mdslmd3i  32356  inin  32540  unidifsnne  32560  disjnf  32594  fnfvor  32636  ofrco  32637  ofrn  32666  ofrn2  32667  ofresid  32669  offinsupp1  32754  tocyccntz  33175  elrgspnlem1  33273  islinds5  33397  ellspds  33398  1arithidomlem2  33566  1arithidom  33567  ply1gsumz  33629  mplvrpmrhm  33661  esplyind  33680  ply1degltdimlem  33728  fedgmullem1  33735  extdgfialglem2  33799  hauseqcn  34004  ofcof  34213  carsgclctunlem1  34423  carsgclctun  34427  sibfof  34446  plymul02  34652  signshf  34694  circlemethhgt  34749  msrid  35688  nepss  35861  bj-inrab2  37072  matunitlindflem1  37756  matunitlindflem2  37757  poimirlem1  37761  poimirlem2  37762  poimirlem3  37763  poimirlem4  37764  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem10  37770  poimirlem11  37771  poimirlem12  37772  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem23  37783  poimirlem24  37784  poimirlem25  37785  poimirlem28  37788  poimirlem29  37789  poimirlem30  37790  poimirlem31  37791  poimirlem32  37792  broucube  37794  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  ftc1anclem3  37835  ftc1anclem5  37837  ftc1anclem6  37838  ftc1anclem8  37840  blbnd  37927  lshpinN  39188  lfladdcl  39270  lflvscl  39276  ldualvaddval  39330  lclkrlem2e  41710  ofun  42434  mplmapghm  42749  fsuppind  42775  fsuppssind  42778  mhphf  42782  mzpclall  42911  mzpindd  42930  dgrsub2  43319  mpaaeu  43334  mendring  43372  ofoafo  43540  ofoacl  43541  ofoaid1  43542  ofoaid2  43543  ofoaass  43544  ofoacom  43545  naddcnff  43546  naddcnffo  43548  naddcnfcom  43550  naddcnfid1  43551  naddcnfass  43553  relexpaddss  43901  ntrkbimka  44221  clsk3nimkb  44223  caofcan  44506  ofmul12  44508  ofdivrec  44509  ofdivcan4  44510  ofdivdiv2  44511  expgrowth  44518  binomcxplemrat  44533  binomcxplemnotnn0  44539  disjf1  45369  dvsinax  46099  dvcosax  46112  dvdivcncf  46113  meadjun  46648  smfmulc1  46982  cjnpoly  47077  f1cof1blem  47262  isubgr0uhgr  48061  uzlidlring  48423  ofaddmndmap  48531  dmatALTbas  48589  dflinc2  48598  fdivmpt  48728  zeroopropdlem  49429  incat  49788  aacllem  49988  amgmwlem  49989