Theorem inidm 3822

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 676	. 2 |- ( ( x e. A /\ x e. A ) <-> x e. A )
2	1	ineqri 3806	1 |- ( A i^i A ) = A

Syntax hints:   = wceq 1483   e. wcel 1990   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  inindi  3830  inindir  3831  uneqin  3878  ssdifeq0  4051  intsng  4512  xpindi  5255  xpindir  5256  resindm  5444  predidm  5702  offval2f  6909  fnfvof  6911  ofres  6913  offval2  6914  ofrfval2  6915  ofco  6917  offveq  6918  offveqb  6919  ofc1  6920  ofc2  6921  caofref  6923  caofrss  6930  caoftrn  6932  suppssof1  7328  suppofss1d  7332  suppofss2d  7333  fisn  8333  dffi3  8337  ofsubeq0  11017  ofnegsub  11018  ofsubge0  11019  seqof  12858  ofccat  13708  incexc  14569  sadeq  15194  smuval2  15204  smumul  15215  ressinbas  15936  pwsle  16152  pwsleval  16153  ghmplusg  18249  gsumzaddlem  18321  gsumzadd  18322  lcomf  18902  lcomfsupp  18903  crng2idl  19239  psrbaglesupp  19368  psrbagaddcl  19370  psrbagcon  19371  psrbaglefi  19372  psrbagconf1o  19374  gsumbagdiaglem  19375  psraddcl  19383  psrvscacl  19393  psrlidm  19403  psrdi  19406  psrdir  19407  mplsubglem  19434  psrbagev1  19510  evlslem3  19514  evlslem1  19515  psrplusgpropd  19606  coe1add  19634  pf1ind  19719  frlmipval  20118  frlmphllem  20119  frlmphl  20120  frlmsslsp  20135  frlmup1  20137  mndvcl  20197  matplusgcell  20239  matsubgcell  20240  mat1dimscm  20281  baspartn  20758  indistopon  20805  epttop  20813  dissnlocfin  21332  ptbasin  21380  snfil  21668  tsmsadd  21950  ust0  22023  ustuqtop1  22045  rrxcph  23180  rrxds  23181  volun  23313  mbfmulc2lem  23414  mbfaddlem  23427  0pledm  23440  i1faddlem  23460  i1fmullem  23461  i1fadd  23462  i1fmul  23463  itg1addlem4  23466  i1fmulclem  23469  i1fmulc  23470  itg1lea  23479  itg1le  23480  mbfi1fseqlem5  23486  mbfi1flimlem  23489  mbfmullem2  23491  xrge0f  23498  itg2ge0  23502  itg2lea  23511  itg2mulclem  23513  itg2mulc  23514  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2mono  23520  itg2i1fseqle  23521  itg2i1fseq  23522  itg2addlem  23525  itg2cnlem1  23528  dvaddf  23705  dvmulf  23706  dvcmulf  23708  dv11cn  23764  plyaddlem1  23969  plyaddlem  23971  coeeulem  23980  coeaddlem  24005  coemulc  24011  dgradd2  24024  dgrcolem2  24030  ofmulrt  24037  plydivlem3  24050  plydivlem4  24051  plydiveu  24053  plyrem  24060  vieta1lem2  24066  elqaalem3  24076  qaa  24078  jensenlem2  24714  jensen  24715  basellem7  24813  basellem9  24815  dchrmulcl  24974  chssoc  28355  chjidm  28379  mdslmd3i  29191  inin  29352  disjnf  29384  ofrn  29441  ofrn2  29442  ofresid  29444  gsumle  29779  hauseqcn  29941  ofcof  30169  carsgclctunlem1  30379  carsgclctun  30383  sibfof  30402  plymul02  30623  signshf  30665  circlemethhgt  30721  msrid  31442  nepss  31599  bj-inrab2  32924  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem28  33437  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  broucube  33443  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  ftc1anclem3  33487  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem8  33492  blbnd  33586  lshpinN  34276  lfladdcl  34358  lflvscl  34364  ldualvaddval  34418  lclkrlem2e  36800  mzpclall  37290  mzpindd  37309  dgrsub2  37705  mpaaeu  37720  mendring  37762  corclrcl  37999  relexpaddss  38010  ntrkbimka  38336  clsk3nimkb  38338  caofcan  38522  ofmul12  38524  ofdivrec  38525  ofdivcan4  38526  ofdivdiv2  38527  expgrowth  38534  binomcxplemrat  38549  binomcxplemnotnn0  38555  disjf1  39369  dvsinax  40127  dvcosax  40141  dvdivcncf  40142  meadjun  40679  smfmulc1  41003  uzlidlring  41929  ofaddmndmap  42122  mndpsuppss  42152  mndpfsupp  42157  dmatALTbas  42190  dflinc2  42199  fdivmpt  42334  aacllem  42547  amgmwlem  42548