Theorem inidm 4197

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

Syntax hints:   = wceq 1537   ∈ wcel 2114   ∩ cin 3937

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945

This theorem is referenced by:  inindi  4205  inindir  4206  uneqin  4257  disjeq0  4407  ssdifeq0  4434  intsng  4913  xpindi  5706  xpindir  5707  resindm  5902  elidinxpid  5914  idinxpresid  5917  predidm  6172  offval2f  7423  fnfvof  7425  ofres  7427  offval2  7428  ofrfval2  7429  ofco  7431  offveq  7432  offveqb  7433  ofc1  7434  ofc2  7435  caofref  7437  caofrss  7444  caoftrn  7446  offsplitfpar  7817  suppssof1  7865  suppofssd  7869  suppofss1d  7870  suppofss2d  7871  fisn  8893  dffi3  8897  ofsubeq0  11637  ofnegsub  11638  ofsubge0  11639  seqof  13430  ofccat  14331  incexc  15194  sadeq  15823  smuval2  15833  smumul  15844  ressinbas  16562  pwsle  16767  pwsleval  16768  ghmplusg  18968  gsumzaddlem  19043  gsumzadd  19044  lcomf  19675  lcomfsupp  19676  crng2idl  20014  psrbaglesupp  20150  psrbagaddcl  20152  psrbagcon  20153  psrbaglefi  20154  psrbagconf1o  20156  gsumbagdiaglem  20157  psraddcl  20165  psrvscacl  20175  psrlidm  20185  psrdi  20188  psrdir  20189  mplsubglem  20216  psrbagev1  20292  evlslem3  20295  evlslem1  20297  psrplusgpropd  20406  coe1add  20434  pf1ind  20520  frlmipval  20925  frlmphllem  20926  frlmphl  20927  frlmsslsp  20942  frlmup1  20944  mndvcl  21004  matplusgcell  21044  matsubgcell  21045  mat1dimscm  21086  baspartn  21564  indistopon  21611  epttop  21619  dissnlocfin  22139  ptbasin  22187  snfil  22474  tsmsadd  22757  ust0  22830  ustuqtop1  22852  rrxcph  23997  rrxds  23998  volun  24148  mbfmulc2lem  24250  mbfaddlem  24263  0pledm  24276  i1faddlem  24296  i1fmullem  24297  i1fadd  24298  i1fmul  24299  itg1addlem4  24302  i1fmulclem  24305  i1fmulc  24306  itg1lea  24315  itg1le  24316  mbfi1fseqlem5  24322  mbfi1flimlem  24325  mbfmullem2  24327  xrge0f  24334  itg2ge0  24338  itg2lea  24347  itg2mulclem  24349  itg2mulc  24350  itg2splitlem  24351  itg2split  24352  itg2monolem1  24353  itg2mono  24356  itg2i1fseqle  24357  itg2i1fseq  24358  itg2addlem  24361  itg2cnlem1  24364  dvaddf  24541  dvmulf  24542  dvcmulf  24544  dv11cn  24600  plyaddlem1  24805  plyaddlem  24807  coeeulem  24816  coeaddlem  24841  coemulc  24847  dgradd2  24860  dgrcolem2  24866  ofmulrt  24873  plydivlem3  24886  plydivlem4  24887  plydiveu  24889  plyrem  24896  vieta1lem2  24902  elqaalem3  24912  qaa  24914  jensenlem2  25567  jensen  25568  basellem7  25666  basellem9  25668  dchrmulcl  25827  chssoc  29275  chjidm  29299  mdslmd3i  30111  inin  30279  unidifsnne  30298  disjnf  30322  ofrn  30388  ofrn2  30389  ofresid  30391  offinsupp1  30465  gsumle  30727  tocyccntz  30788  islinds5  30934  ellspds  30935  fedgmullem1  31027  hauseqcn  31140  ofcof  31368  carsgclctunlem1  31577  carsgclctun  31581  sibfof  31600  plymul02  31818  signshf  31860  circlemethhgt  31916  msrid  32794  nepss  32950  bj-inrab2  34248  matunitlindflem1  34890  matunitlindflem2  34891  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem28  34922  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  poimirlem32  34926  broucube  34928  itg2addnclem  34945  itg2addnclem3  34947  itg2addnc  34948  ftc1anclem3  34971  ftc1anclem5  34973  ftc1anclem6  34974  ftc1anclem8  34976  blbnd  35067  lshpinN  36127  lfladdcl  36209  lflvscl  36215  ldualvaddval  36269  lclkrlem2e  38649  mzpclall  39331  mzpindd  39350  dgrsub2  39742  mpaaeu  39757  mendring  39799  relexpaddss  40070  ntrkbimka  40395  clsk3nimkb  40397  caofcan  40662  ofmul12  40664  ofdivrec  40665  ofdivcan4  40666  ofdivdiv2  40667  expgrowth  40674  binomcxplemrat  40689  binomcxplemnotnn0  40695  disjf1  41450  dvsinax  42204  dvcosax  42218  dvdivcncf  42219  meadjun  42751  smfmulc1  43078  uzlidlring  44207  ofaddmndmap  44399  mndpsuppss  44426  mndpfsupp  44431  dmatALTbas  44463  dflinc2  44472  fdivmpt  44607  aacllem  44909  amgmwlem  44910