Theorem inidm 4248

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

Syntax hints:   = wceq 1537   ∈ wcel 2108   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  inindi  4256  inindir  4257  uneqin  4308  disjeq0  4479  ssdifeq0  4510  intsng  5007  xpindi  5858  xpindir  5859  resindm  6059  elidinxpid  6074  idinxpresid  6077  predidm  6358  offval2f  7729  fnfvof  7731  ofres  7733  offval2  7734  ofrfval2  7735  coof  7737  ofco  7738  offveq  7739  offveqb  7740  ofc1  7741  ofc2  7742  caofref  7744  caofrss  7751  caoftrn  7753  offsplitfpar  8160  suppssof1  8240  suppofssd  8244  suppofss1d  8245  suppofss2d  8246  fisn  9496  dffi3  9500  ofsubeq0  12290  ofnegsub  12291  ofsubge0  12292  seqof  14110  ofccat  15018  incexc  15885  sadeq  16518  smuval2  16528  smumul  16539  ressinbas  17304  pwsle  17552  pwsleval  17553  mndvcl  18832  ghmplusg  19888  gsumzaddlem  19963  gsumzadd  19964  pwspjmhmmgpd  20351  lcomf  20921  crng2idl  21314  frlmipval  21822  frlmphllem  21823  frlmphl  21824  frlmsslsp  21839  frlmup1  21841  psrbaglesupp  21965  psrbagaddcl  21967  psrbagcon  21968  psrbaglefi  21969  psrbagleadd1  21971  psrbagconf1o  21972  gsumbagdiaglem  21973  psraddcl  21981  psraddclOLD  21982  psrvscacl  21994  psrlidm  22005  psrdi  22008  psrdir  22009  psrascl  22022  mplsubglem  22042  psrbagev1  22124  evlslem3  22127  evlslem1  22129  mhpmulcl  22176  psdmplcl  22189  psdadd  22190  psdmul  22193  psrplusgpropd  22258  coe1add  22288  pf1ind  22380  evls1fpws  22394  matplusgcell  22460  matsubgcell  22461  mat1dimscm  22502  baspartn  22982  indistopon  23029  epttop  23037  dissnlocfin  23558  ptbasin  23606  snfil  23893  tsmsadd  24176  ust0  24249  ustuqtop1  24271  rrxcph  25445  rrxds  25446  volun  25599  mbfmulc2lem  25701  mbfaddlem  25714  0pledm  25727  i1faddlem  25747  i1fmullem  25748  i1fadd  25749  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  i1fmulclem  25757  i1fmulc  25758  itg1lea  25767  itg1le  25768  mbfi1fseqlem5  25774  mbfi1flimlem  25777  mbfmullem2  25779  xrge0f  25786  itg2ge0  25790  itg2lea  25799  itg2mulclem  25801  itg2mulc  25802  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2mono  25808  itg2i1fseqle  25809  itg2i1fseq  25810  itg2addlem  25813  itg2cnlem1  25816  dvaddf  25999  dvmulf  26000  dvcmulf  26002  dv11cn  26060  plyaddlem1  26272  plyaddlem  26274  coeeulem  26283  coeaddlem  26308  coemulc  26314  dgradd2  26328  dgrcolem2  26334  ofmulrt  26341  plydivlem3  26355  plydivlem4  26356  plydiveu  26358  plyrem  26365  vieta1lem2  26371  elqaalem3  26381  qaa  26383  jensenlem2  27049  jensen  27050  basellem7  27148  basellem9  27150  dchrmulcl  27311  chssoc  31528  chjidm  31552  mdslmd3i  32364  inin  32545  unidifsnne  32564  disjnf  32592  ofrn  32658  ofrn2  32659  ofresid  32661  offinsupp1  32741  gsumle  33074  tocyccntz  33137  islinds5  33360  ellspds  33361  1arithidomlem2  33529  1arithidom  33530  ply1gsumz  33584  ply1degltdimlem  33635  fedgmullem1  33642  hauseqcn  33844  ofcof  34071  carsgclctunlem1  34282  carsgclctun  34286  sibfof  34305  plymul02  34523  signshf  34565  circlemethhgt  34620  msrid  35513  nepss  35680  bj-inrab2  36894  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem28  37608  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  broucube  37614  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  ftc1anclem3  37655  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem8  37660  blbnd  37747  lshpinN  38945  lfladdcl  39027  lflvscl  39033  ldualvaddval  39087  lclkrlem2e  41468  ofun  42231  mplmapghm  42511  evlsvvval  42518  fsuppind  42545  fsuppssind  42548  mhphf  42552  mzpclall  42683  mzpindd  42702  dgrsub2  43092  mpaaeu  43107  mendring  43149  ofoafo  43318  ofoacl  43319  ofoaid1  43320  ofoaid2  43321  ofoaass  43322  ofoacom  43323  naddcnff  43324  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  naddcnfass  43331  relexpaddss  43680  ntrkbimka  44000  clsk3nimkb  44002  caofcan  44292  ofmul12  44294  ofdivrec  44295  ofdivcan4  44296  ofdivdiv2  44297  expgrowth  44304  binomcxplemrat  44319  binomcxplemnotnn0  44325  disjf1  45090  dvsinax  45834  dvcosax  45847  dvdivcncf  45848  meadjun  46383  smfmulc1  46717  f1cof1blem  46989  isubgr0uhgr  47743  uzlidlring  47958  ofaddmndmap  48068  mndpsuppss  48096  dmatALTbas  48130  dflinc2  48139  fdivmpt  48274  aacllem  48895  amgmwlem  48896