Theorem inidm 4234

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

Syntax hints:   = wceq 1536   ∈ wcel 2105   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969

This theorem is referenced by:  inindi  4242  inindir  4243  uneqin  4294  disjeq0  4461  ssdifeq0  4492  intsng  4987  xpindi  5846  xpindir  5847  resindm  6049  elidinxpid  6064  idinxpresid  6067  predidm  6348  offval2f  7711  fnfvof  7713  ofres  7715  offval2  7716  ofrfval2  7717  coof  7720  ofco  7721  offveq  7722  offveqb  7723  ofc1  7724  ofc2  7725  caofref  7727  caofrss  7734  caoftrn  7736  offsplitfpar  8142  suppssof1  8222  suppofssd  8226  suppofss1d  8227  suppofss2d  8228  fisn  9464  dffi3  9468  ofsubeq0  12260  ofnegsub  12261  ofsubge0  12262  seqof  14096  ofccat  15004  incexc  15869  sadeq  16505  smuval2  16515  smumul  16526  ressinbas  17290  pwsle  17538  pwsleval  17539  mndpsuppss  18790  mndvcl  18822  ghmplusg  19878  gsumzaddlem  19953  gsumzadd  19954  pwspjmhmmgpd  20341  lcomf  20915  crng2idl  21308  frlmipval  21816  frlmphllem  21817  frlmphl  21818  frlmsslsp  21833  frlmup1  21835  psrbaglesupp  21959  psrbagaddcl  21961  psrbagcon  21962  psrbaglefi  21963  psrbagleadd1  21965  psrbagconf1o  21966  gsumbagdiaglem  21967  psraddcl  21975  psraddclOLD  21976  psrvscacl  21988  psrlidm  21999  psrdi  22002  psrdir  22003  psrascl  22016  mplsubglem  22036  psrbagev1  22118  evlslem3  22121  evlslem1  22123  mhpmulcl  22170  psdmplcl  22183  psdadd  22184  psdmul  22187  psrplusgpropd  22252  coe1add  22282  pf1ind  22374  evls1fpws  22388  matplusgcell  22454  matsubgcell  22455  mat1dimscm  22496  baspartn  22976  indistopon  23023  epttop  23031  dissnlocfin  23552  ptbasin  23600  snfil  23887  tsmsadd  24170  ust0  24243  ustuqtop1  24265  rrxcph  25439  rrxds  25440  volun  25593  mbfmulc2lem  25695  mbfaddlem  25708  0pledm  25721  i1faddlem  25741  i1fmullem  25742  i1fadd  25743  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  i1fmulclem  25751  i1fmulc  25752  itg1lea  25761  itg1le  25762  mbfi1fseqlem5  25768  mbfi1flimlem  25771  mbfmullem2  25773  xrge0f  25780  itg2ge0  25784  itg2lea  25793  itg2mulclem  25795  itg2mulc  25796  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2addlem  25807  itg2cnlem1  25810  dvaddf  25993  dvmulf  25994  dvcmulf  25996  dv11cn  26054  plyaddlem1  26266  plyaddlem  26268  coeeulem  26277  coeaddlem  26302  coemulc  26308  dgradd2  26322  dgrcolem2  26328  ofmulrt  26337  plydivlem3  26351  plydivlem4  26352  plydiveu  26354  plyrem  26361  vieta1lem2  26367  elqaalem3  26377  qaa  26379  jensenlem2  27045  jensen  27046  basellem7  27144  basellem9  27146  dchrmulcl  27307  chssoc  31524  chjidm  31548  mdslmd3i  32360  inin  32543  unidifsnne  32561  disjnf  32589  ofrn  32655  ofrn2  32656  ofresid  32658  offinsupp1  32744  gsumle  33083  tocyccntz  33146  elrgspnlem1  33231  islinds5  33374  ellspds  33375  1arithidomlem2  33543  1arithidom  33544  ply1gsumz  33598  ply1degltdimlem  33649  fedgmullem1  33656  hauseqcn  33858  ofcof  34087  carsgclctunlem1  34298  carsgclctun  34302  sibfof  34321  plymul02  34539  signshf  34581  circlemethhgt  34636  msrid  35529  nepss  35697  bj-inrab2  36910  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem28  37634  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  broucube  37640  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  ftc1anclem3  37681  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem8  37686  blbnd  37773  lshpinN  38970  lfladdcl  39052  lflvscl  39058  ldualvaddval  39112  lclkrlem2e  41493  ofun  42255  mplmapghm  42542  evlsvvval  42549  fsuppind  42576  fsuppssind  42579  mhphf  42583  mzpclall  42714  mzpindd  42733  dgrsub2  43123  mpaaeu  43138  mendring  43176  ofoafo  43345  ofoacl  43346  ofoaid1  43347  ofoaid2  43348  ofoaass  43349  ofoacom  43350  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfass  43358  relexpaddss  43707  ntrkbimka  44027  clsk3nimkb  44029  caofcan  44318  ofmul12  44320  ofdivrec  44321  ofdivcan4  44322  ofdivdiv2  44323  expgrowth  44330  binomcxplemrat  44345  binomcxplemnotnn0  44351  disjf1  45125  dvsinax  45868  dvcosax  45881  dvdivcncf  45882  meadjun  46417  smfmulc1  46751  f1cof1blem  47023  isubgr0uhgr  47796  uzlidlring  48078  ofaddmndmap  48187  dmatALTbas  48246  dflinc2  48255  fdivmpt  48389  aacllem  49031  amgmwlem  49032