Theorem inidm 4084

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

Syntax hints:   = wceq 1507   ∈ wcel 2050   ∩ cin 3830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-in 3838

This theorem is referenced by:  inindi  4092  inindir  4093  uneqin  4144  disjeq0  4289  ssdifeq0  4316  intsng  4785  xpindi  5555  xpindir  5556  resindm  5747  elidinxpid  5759  predidm  6010  offval2f  7241  fnfvof  7243  ofres  7245  offval2  7246  ofrfval2  7247  ofco  7249  offveq  7250  offveqb  7251  ofc1  7252  ofc2  7253  caofref  7255  caofrss  7262  caoftrn  7264  suppssof1  7668  suppofssd  7672  suppofss1d  7673  suppofss2d  7674  fisn  8688  dffi3  8692  ofsubeq0  11438  ofnegsub  11439  ofsubge0  11440  seqof  13245  ofccat  14193  incexc  15055  sadeq  15684  smuval2  15694  smumul  15705  ressinbas  16419  pwsle  16624  pwsleval  16625  ghmplusg  18725  gsumzaddlem  18797  gsumzadd  18798  lcomf  19398  lcomfsupp  19399  crng2idl  19736  psrbaglesupp  19865  psrbagaddcl  19867  psrbagcon  19868  psrbaglefi  19869  psrbagconf1o  19871  gsumbagdiaglem  19872  psraddcl  19880  psrvscacl  19890  psrlidm  19900  psrdi  19903  psrdir  19904  mplsubglem  19931  psrbagev1  20006  evlslem3  20010  evlslem1  20011  psrplusgpropd  20110  coe1add  20138  pf1ind  20223  frlmipval  20628  frlmphllem  20629  frlmphl  20630  frlmsslsp  20645  frlmup1  20647  mndvcl  20707  matplusgcell  20749  matsubgcell  20750  mat1dimscm  20791  baspartn  21269  indistopon  21316  epttop  21324  dissnlocfin  21844  ptbasin  21892  snfil  22179  tsmsadd  22461  ust0  22534  ustuqtop1  22556  rrxcph  23701  rrxds  23702  volun  23852  mbfmulc2lem  23954  mbfaddlem  23967  0pledm  23980  i1faddlem  24000  i1fmullem  24001  i1fadd  24002  i1fmul  24003  itg1addlem4  24006  i1fmulclem  24009  i1fmulc  24010  itg1lea  24019  itg1le  24020  mbfi1fseqlem5  24026  mbfi1flimlem  24029  mbfmullem2  24031  xrge0f  24038  itg2ge0  24042  itg2lea  24051  itg2mulclem  24053  itg2mulc  24054  itg2splitlem  24055  itg2split  24056  itg2monolem1  24057  itg2mono  24060  itg2i1fseqle  24061  itg2i1fseq  24062  itg2addlem  24065  itg2cnlem1  24068  dvaddf  24245  dvmulf  24246  dvcmulf  24248  dv11cn  24304  plyaddlem1  24509  plyaddlem  24511  coeeulem  24520  coeaddlem  24545  coemulc  24551  dgradd2  24564  dgrcolem2  24570  ofmulrt  24577  plydivlem3  24590  plydivlem4  24591  plydiveu  24593  plyrem  24600  vieta1lem2  24606  elqaalem3  24616  qaa  24618  jensenlem2  25270  jensen  25271  basellem7  25369  basellem9  25371  dchrmulcl  25530  chssoc  29057  chjidm  29081  mdslmd3i  29893  inin  30056  disjnf  30090  ofrn  30151  ofrn2  30152  ofresid  30154  offinsupp1  30218  gsumle  30522  islinds5  30605  ellspds  30606  fedgmullem1  30654  hauseqcn  30782  ofcof  31010  carsgclctunlem1  31220  carsgclctun  31224  sibfof  31243  plymul02  31462  signshf  31506  circlemethhgt  31562  msrid  32312  nepss  32468  bj-inrab2  33741  matunitlindflem1  34329  matunitlindflem2  34330  poimirlem1  34334  poimirlem2  34335  poimirlem3  34336  poimirlem4  34337  poimirlem6  34339  poimirlem7  34340  poimirlem8  34341  poimirlem10  34343  poimirlem11  34344  poimirlem12  34345  poimirlem16  34349  poimirlem17  34350  poimirlem19  34352  poimirlem20  34353  poimirlem23  34356  poimirlem24  34357  poimirlem25  34358  poimirlem28  34361  poimirlem29  34362  poimirlem30  34363  poimirlem31  34364  poimirlem32  34365  broucube  34367  itg2addnclem  34384  itg2addnclem3  34386  itg2addnc  34387  ftc1anclem3  34410  ftc1anclem5  34412  ftc1anclem6  34413  ftc1anclem8  34415  blbnd  34507  lshpinN  35570  lfladdcl  35652  lflvscl  35658  ldualvaddval  35712  lclkrlem2e  38092  mzpclall  38719  mzpindd  38738  dgrsub2  39131  mpaaeu  39146  mendring  39188  corclrcl  39415  relexpaddss  39426  ntrkbimka  39751  clsk3nimkb  39753  caofcan  40071  ofmul12  40073  ofdivrec  40074  ofdivcan4  40075  ofdivdiv2  40076  expgrowth  40083  binomcxplemrat  40098  binomcxplemnotnn0  40104  disjf1  40868  dvsinax  41628  dvcosax  41642  dvdivcncf  41643  meadjun  42176  smfmulc1  42503  uzlidlring  43565  ofaddmndmap  43757  mndpsuppss  43786  mndpfsupp  43791  dmatALTbas  43824  dflinc2  43833  fdivmpt  43969  aacllem  44270  amgmwlem  44271