Theorem inidm 3672

Description: Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
inidm	|- ( A i^i A ) = A

Proof of Theorem inidm

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		anidm 649	. 2 |- ( ( x e. A /\ x e. A ) <-> x e. A )
2	1	ineqri 3657	1 |- ( A i^i A ) = A

Syntax hints:   = wceq 1438   e. wcel 1869   i^i cin 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444

This theorem is referenced by:  inindi  3680  inindir  3681  uneqin  3725  ssdifeq0  3879  intsng  4289  xpindi  4985  xpindir  4986  resindm  5166  predidm  5419  offval2f  6555  fnfvof  6557  ofres  6559  offval2  6560  ofrfval2  6561  ofco  6563  offveq  6564  offveqb  6565  ofc1  6566  ofc2  6567  caofref  6569  caofrss  6576  caoftrn  6578  suppssof1  6957  suppofss1d  6961  suppofss2d  6962  fisn  7945  dffi3  7949  ofsubeq0  10608  ofnegsub  10609  ofsubge0  10610  seqof  12271  incexc  13888  sadeq  14439  smuval2  14449  smumul  14460  ressinbas  15178  pwsle  15383  pwsleval  15384  ghmplusg  17477  gsumzaddlem  17547  gsumzadd  17548  lcomf  18120  lcomfsupp  18121  crng2idl  18456  psrbaglesupp  18585  psrbagaddcl  18587  psrbagcon  18588  psrbaglefi  18589  psrbagconf1o  18591  gsumbagdiaglem  18592  psraddcl  18600  psrvscacl  18610  psrlidm  18620  psrdi  18623  psrdir  18624  mplsubglem  18651  psrbagev1  18726  evlslem3  18730  evlslem1  18731  psrplusgpropd  18822  coe1add  18850  pf1ind  18936  frlmipval  19329  frlmphllem  19330  frlmphl  19331  frlmsslsp  19346  frlmup1  19348  mndvcl  19408  matplusgcell  19450  matsubgcell  19451  mat1dimscm  19492  baspartn  19961  indistopon  20008  epttop  20016  dissnlocfin  20536  ptbasin  20584  snfil  20871  tsmsadd  21153  ust0  21226  ustuqtop1  21248  rrxcph  22343  rrxds  22344  volun  22490  mbfmulc2lem  22595  mbfaddlem  22608  0pledm  22623  i1faddlem  22643  i1fmullem  22644  i1fadd  22645  i1fmul  22646  itg1addlem4  22649  i1fmulclem  22652  i1fmulc  22653  itg1lea  22662  itg1le  22663  mbfi1fseqlem5  22669  mbfi1flimlem  22672  mbfmullem2  22674  xrge0f  22681  itg2ge0  22685  itg2lea  22694  itg2mulclem  22696  itg2mulc  22697  itg2splitlem  22698  itg2split  22699  itg2monolem1  22700  itg2mono  22703  itg2i1fseqle  22704  itg2i1fseq  22705  itg2addlem  22708  itg2cnlem1  22711  dvaddf  22888  dvmulf  22889  dvcmulf  22891  dv11cn  22945  plyaddlem1  23159  plyaddlem  23161  coeeulem  23170  coeaddlem  23195  coemulc  23201  dgradd2  23214  dgrcolem2  23220  ofmulrt  23227  plydivlem3  23240  plydivlem4  23241  plydiveu  23243  plyrem  23250  vieta1lem2  23256  elqaalem3  23266  elqaalem3OLD  23269  qaa  23271  jensenlem2  23905  jensen  23906  basellem7  24005  basellem9  24007  dchrmulcl  24169  chssoc  27141  chjidm  27165  mdslmd3i  27977  inin  28142  disjnf  28177  ofrn  28236  ofrn2  28237  ofresid  28239  gsumle  28543  hauseqcn  28703  ofcof  28930  carsgclctunlem1  29151  carsgclctun  29155  sibfof  29175  ofccat  29431  plymul02  29437  signshf  29479  msrid  30185  nepss  30352  bj-inrab2  31494  poimirlem1  31899  poimirlem2  31900  poimirlem3  31901  poimirlem4  31902  poimirlem6  31904  poimirlem7  31905  poimirlem8  31906  poimirlem10  31908  poimirlem11  31909  poimirlem12  31910  poimirlem16  31914  poimirlem17  31915  poimirlem19  31917  poimirlem20  31918  poimirlem23  31921  poimirlem24  31922  poimirlem25  31923  poimirlem28  31926  poimirlem29  31927  poimirlem30  31928  poimirlem31  31929  poimirlem32  31930  broucube  31932  itg2addnclem  31951  itg2addnclem3  31953  itg2addnc  31954  ftc1anclem3  31977  ftc1anclem5  31979  ftc1anclem6  31980  ftc1anclem8  31982  blbnd  32077  lshpinN  32518  lfladdcl  32600  lflvscl  32606  ldualvaddval  32660  lclkrlem2e  35042  mzpclall  35532  mzpindd  35551  dgrsub2  35958  mpaaeu  35980  mendring  36022  corclrcl  36203  relexpaddss  36214  caofcan  36574  ofmul12  36576  ofdivrec  36577  ofdivcan4  36578  ofdivdiv2  36579  expgrowth  36586  binomcxplemrat  36601  binomcxplemnotnn0  36607  disjf1  37351  dvsinax  37647  dvcosax  37662  dvdivcncf  37663  meadjun  38123  uzlidlring  39271  ofaddmndmap  39469  mndpsuppss  39500  mndpfsupp  39505  dmatALTbas  39538  dflinc2  39547  fdivmpt  39695  aacllem  39884