Theorem inidm 4207

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

Syntax hints:   = wceq 1540   ∈ wcel 2109   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938

This theorem is referenced by:  inindi  4215  inindir  4216  uneqin  4269  disjeq0  4436  ssdifeq0  4467  intsng  4964  xpindi  5818  xpindir  5819  resindm  6022  elidinxpid  6037  idinxpresid  6040  predidm  6320  offval2f  7691  fnfvof  7693  ofres  7695  offval2  7696  ofrfval2  7697  coof  7700  ofco  7701  offveq  7702  offveqb  7703  ofc1  7704  ofc2  7705  caofref  7707  caofrss  7715  caoftrn  7717  offsplitfpar  8123  suppssof1  8203  suppofssd  8207  suppofss1d  8208  suppofss2d  8209  fisn  9444  dffi3  9448  ofsubeq0  12242  ofnegsub  12243  ofsubge0  12244  seqof  14082  ofccat  14993  incexc  15858  sadeq  16496  smuval2  16506  smumul  16517  ressinbas  17271  pwsle  17511  pwsleval  17512  mndpsuppss  18748  mndvcl  18780  ghmplusg  19832  gsumzaddlem  19907  gsumzadd  19908  pwspjmhmmgpd  20293  lcomf  20863  crng2idl  21247  frlmipval  21744  frlmphllem  21745  frlmphl  21746  frlmsslsp  21761  frlmup1  21763  psrbaglesupp  21887  psrbagaddcl  21889  psrbagcon  21890  psrbaglefi  21891  psrbagleadd1  21893  psrbagconf1o  21894  gsumbagdiaglem  21895  psraddcl  21903  psraddclOLD  21904  psrvscacl  21916  psrlidm  21927  psrdi  21930  psrdir  21931  psrascl  21944  mplsubglem  21964  psrbagev1  22040  evlslem3  22043  evlslem1  22045  mhpmulcl  22092  psdmplcl  22105  psdadd  22106  psdmul  22109  psdmvr  22112  psrplusgpropd  22176  coe1add  22206  pf1ind  22298  evls1fpws  22312  matplusgcell  22376  matsubgcell  22377  mat1dimscm  22418  baspartn  22897  indistopon  22944  epttop  22952  dissnlocfin  23472  ptbasin  23520  snfil  23807  tsmsadd  24090  ust0  24163  ustuqtop1  24185  rrxcph  25349  rrxds  25350  volun  25503  mbfmulc2lem  25605  mbfaddlem  25618  0pledm  25631  i1faddlem  25651  i1fmullem  25652  i1fadd  25653  i1fmul  25654  itg1addlem4  25657  i1fmulclem  25660  i1fmulc  25661  itg1lea  25670  itg1le  25671  mbfi1fseqlem5  25677  mbfi1flimlem  25680  mbfmullem2  25682  xrge0f  25689  itg2ge0  25693  itg2lea  25702  itg2mulclem  25704  itg2mulc  25705  itg2splitlem  25706  itg2split  25707  itg2monolem1  25708  itg2mono  25711  itg2i1fseqle  25712  itg2i1fseq  25713  itg2addlem  25716  itg2cnlem1  25719  dvaddf  25902  dvmulf  25903  dvcmulf  25905  dv11cn  25963  plyaddlem1  26175  plyaddlem  26177  coeeulem  26186  coeaddlem  26211  coemulc  26217  dgradd2  26231  dgrcolem2  26237  ofmulrt  26246  plydivlem3  26260  plydivlem4  26261  plydiveu  26263  plyrem  26270  vieta1lem2  26276  elqaalem3  26286  qaa  26288  jensenlem2  26955  jensen  26956  basellem7  27054  basellem9  27056  dchrmulcl  27217  chssoc  31482  chjidm  31506  mdslmd3i  32318  inin  32502  unidifsnne  32522  disjnf  32556  ofrn  32622  ofrn2  32623  ofresid  32625  offinsupp1  32709  gsumle  33097  tocyccntz  33160  elrgspnlem1  33242  islinds5  33387  ellspds  33388  1arithidomlem2  33556  1arithidom  33557  ply1gsumz  33613  ply1degltdimlem  33667  fedgmullem1  33674  hauseqcn  33934  ofcof  34143  carsgclctunlem1  34354  carsgclctun  34358  sibfof  34377  plymul02  34583  signshf  34625  circlemethhgt  34680  msrid  35572  nepss  35740  bj-inrab2  36951  matunitlindflem1  37645  matunitlindflem2  37646  poimirlem1  37650  poimirlem2  37651  poimirlem3  37652  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem10  37659  poimirlem11  37660  poimirlem12  37661  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem23  37672  poimirlem24  37673  poimirlem25  37674  poimirlem28  37677  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  poimirlem32  37681  broucube  37683  itg2addnclem  37700  itg2addnclem3  37702  itg2addnc  37703  ftc1anclem3  37724  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem8  37729  blbnd  37816  lshpinN  39012  lfladdcl  39094  lflvscl  39100  ldualvaddval  39154  lclkrlem2e  41535  ofun  42254  mplmapghm  42554  evlsvvval  42561  fsuppind  42588  fsuppssind  42591  mhphf  42595  mzpclall  42725  mzpindd  42744  dgrsub2  43134  mpaaeu  43149  mendring  43187  ofoafo  43355  ofoacl  43356  ofoaid1  43357  ofoaid2  43358  ofoaass  43359  ofoacom  43360  naddcnff  43361  naddcnffo  43363  naddcnfcom  43365  naddcnfid1  43366  naddcnfass  43368  relexpaddss  43717  ntrkbimka  44037  clsk3nimkb  44039  caofcan  44322  ofmul12  44324  ofdivrec  44325  ofdivcan4  44326  ofdivdiv2  44327  expgrowth  44334  binomcxplemrat  44349  binomcxplemnotnn0  44355  disjf1  45187  dvsinax  45922  dvcosax  45935  dvdivcncf  45936  meadjun  46471  smfmulc1  46805  f1cof1blem  47083  isubgr0uhgr  47866  uzlidlring  48190  ofaddmndmap  48298  dmatALTbas  48357  dflinc2  48366  fdivmpt  48500  zeroopropdlem  49139  incat  49458  aacllem  49645  amgmwlem  49646