Theorem inidm 4172

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 575	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	ineqri 4158	1 ⊢ (𝐴 ∩ 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  inindi  4180  inindir  4181  uneqin  4235  disjeq0  4409  ssdifeq0  4442  intsng  4943  xpindi  5814  xpindir  5815  resindmOLD  6025  elidinxpid  6042  idinxpresid  6045  predidm  6325  offval2f  7695  fnfvof  7697  ofres  7699  offval2  7700  ofrfval2  7701  coof  7704  ofco  7705  offveq  7706  offveqb  7707  ofc1  7708  ofc2  7709  caofref  7711  caofrss  7719  caoftrn  7721  offsplitfpar  8118  suppssof1  8199  suppofssd  8203  suppofss1d  8204  suppofss2d  8205  fisn  9401  dffi3  9405  ofsubeq0  12261  ofnegsub  12262  ofsubge0  12263  seqof  14145  ofccat  15064  incexc  15948  sadeq  16584  smuval2  16594  smumul  16605  ressinbas  17359  pwsle  17600  pwsleval  17601  mndpsuppss  18895  mndvcl  18928  ghmplusg  19996  gsumzaddlem  20071  gsumzadd  20072  gsumle  20295  pwspjmhmmgpd  20493  lcomf  21112  crng2idl  21512  frlmipval  22021  frlmphllem  22022  frlmphl  22023  frlmsslsp  22038  frlmup1  22040  psrbaglesupp  22166  psrbagaddcl  22168  psrbagcon  22169  psrbaglefi  22170  psrbagleadd1  22172  psrbagconf1o  22173  gsumbagdiaglem  22175  psraddcl  22183  psrvscacl  22195  psrlidm  22205  psrdi  22208  psrdir  22209  psrascl  22222  mplsubglem  22242  psrbagev1  22322  evlslem3  22325  evlslem1  22327  evlsvvval  22338  mplmapghm  22367  mhpmulcl  22406  psdmplcl  22419  psdadd  22420  psdmul  22423  psdmvr  22426  psrplusgpropd  22489  coe1add  22519  pf1ind  22609  evls1fpws  22623  matplusgcell  22684  matsubgcell  22685  mat1dimscm  22726  matunitlindflem1  22930  matunitlindflem2  22931  baspartn  23208  indistopon  23255  epttop  23263  dissnlocfin  23784  ptbasin  23832  snfil  24119  tsmsadd  24402  ust0  24475  ustuqtop1  24496  rrxcph  25649  rrxds  25650  volun  25802  mbfmulc2lem  25904  mbfaddlem  25917  0pledm  25930  i1faddlem  25950  i1fmullem  25951  i1fadd  25952  i1fmul  25953  itg1addlem4  25956  i1fmulclem  25959  i1fmulc  25960  itg1lea  25969  itg1le  25970  mbfi1fseqlem5  25976  mbfi1flimlem  25979  mbfmullem2  25981  xrge0f  25988  itg2ge0  25992  itg2lea  26001  itg2mulclem  26003  itg2mulc  26004  itg2splitlem  26005  itg2split  26006  itg2monolem1  26007  itg2mono  26010  itg2i1fseqle  26011  itg2i1fseq  26012  itg2addlem  26015  itg2cnlem1  26018  dvaddf  26198  dvmulf  26199  dvcmulf  26201  dv11cn  26257  plyaddlem1  26468  plyaddlem  26470  coeeulem  26479  coeaddlem  26504  coemulc  26510  dgradd2  26523  dgrcolem2  26529  ofmulrt  26538  plymul02  26539  plydivlem3  26554  plydivlem4  26555  plydiveu  26557  plyrem  26564  rnplynfin  26568  vieta1lem2  26572  elqaalem3  26582  qaa  26585  jensenlem2  27253  jensen  27254  basellem7  27352  basellem9  27354  dchrmulcl  27514  chssoc  32006  chjidm  32030  mdslmd3i  32842  inin  33020  unidifsnne  33040  disjnf  33072  fnfvor  33111  ofrco  33112  ofrn  33141  ofrn2  33142  ofresid  33144  offinsupp1  33226  tocyccntz  33613  elrgspnlem1  33711  islinds5  33831  ellspds  33832  1arithidomlem2  33976  1arithidom  33977  ply1gsumz  34039  0mplrim  34054  selvply1rhmlemb  34059  selvply1rhmlem4  34063  mplvrpmrhm  34087  esplyind  34115  ply1degltdimlem  34162  fedgmullem1  34169  extdgfialglem2  34233  hauseqcn  34438  ofcof  34647  carsgclctunlem1  34858  carsgclctun  34862  sibfof  34881  signshf  35126  circlemethhgt  35181  msrid  36154  nepss  36327  bj-inrab2  37686  poimirlem1  38384  poimirlem2  38385  poimirlem4  38387  poimirlem6  38389  poimirlem7  38390  poimirlem8  38391  poimirlem10  38393  poimirlem11  38394  poimirlem12  38395  poimirlem16  38399  poimirlem17  38400  poimirlem19  38402  poimirlem20  38403  poimirlem23  38406  poimirlem24  38407  poimirlem25  38408  poimirlem28  38411  poimirlem29  38412  poimirlem30  38413  poimirlem31  38414  poimirlem32  38415  broucube  38417  itg2addnclem  38434  itg2addnclem3  38436  itg2addnc  38437  ftc1anclem3  38458  ftc1anclem5  38460  ftc1anclem6  38461  ftc1anclem8  38463  blbnd  38551  disjimeceqim  39566  lshpinN  39876  lfladdcl  39958  lflvscl  39964  ldualvaddval  40018  lclkrlem2e  42398  ofun  43119  fsuppind  43450  fsuppssind  43453  mhphf  43457  mzpclall  43586  mzpindd  43605  dgrsub2  43990  mpaaeu  44005  mendring  44043  ofoafo  44211  ofoacl  44212  ofoaid1  44213  ofoaid2  44214  ofoaass  44215  ofoacom  44216  naddcnff  44217  naddcnffo  44219  naddcnfcom  44221  naddcnfid1  44222  naddcnfass  44224  relexpaddss  44572  ntrkbimka  44892  clsk3nimkb  44894  caofcan  45161  ofmul12  45163  ofdivrec  45164  ofdivcan4  45165  ofdivdiv2  45166  expgrowth  45173  binomcxplemrat  45188  binomcxplemnotnn0  45194  disjf1  46029  dvsinax  46755  dvcosax  46768  dvdivcncf  46769  meadjun  47304  smfmulc1  47638  cjnpoly  47771  f1cof1blem  47976  isubgr0uhgr  48803  uzlidlring  49164  ofaddmndmap  49287  dmatALTbas  49345  dflinc2  49354  fdivmpt  49484  zeroopropdlem  50182  incat  50541  aacllem  50786  veroquadmodzerod  50831  amgmwlem  50834