Theorem inidm 3632

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

Syntax hints:   = wceq 1452   e. wcel 1904   i^i cin 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397

This theorem is referenced by:  inindi  3640  inindir  3641  uneqin  3685  ssdifeq0  3841  intsng  4261  xpindi  4973  xpindir  4974  resindm  5155  predidm  5409  offval2f  6562  fnfvof  6564  ofres  6566  offval2  6567  ofrfval2  6568  ofco  6570  offveq  6571  offveqb  6572  ofc1  6573  ofc2  6574  caofref  6576  caofrss  6583  caoftrn  6585  suppssof1  6967  suppofss1d  6971  suppofss2d  6972  fisn  7959  dffi3  7963  ofsubeq0  10628  ofnegsub  10629  ofsubge0  10630  seqof  12308  incexc  13972  sadeq  14525  smuval2  14535  smumul  14546  ressinbas  15263  pwsle  15468  pwsleval  15469  ghmplusg  17562  gsumzaddlem  17632  gsumzadd  17633  lcomf  18205  lcomfsupp  18206  crng2idl  18540  psrbaglesupp  18669  psrbagaddcl  18671  psrbagcon  18672  psrbaglefi  18673  psrbagconf1o  18675  gsumbagdiaglem  18676  psraddcl  18684  psrvscacl  18694  psrlidm  18704  psrdi  18707  psrdir  18708  mplsubglem  18735  psrbagev1  18810  evlslem3  18814  evlslem1  18815  psrplusgpropd  18906  coe1add  18934  pf1ind  19020  frlmipval  19414  frlmphllem  19415  frlmphl  19416  frlmsslsp  19431  frlmup1  19433  mndvcl  19493  matplusgcell  19535  matsubgcell  19536  mat1dimscm  19577  baspartn  20046  indistopon  20093  epttop  20101  dissnlocfin  20621  ptbasin  20669  snfil  20957  tsmsadd  21239  ust0  21312  ustuqtop1  21334  rrxcph  22429  rrxds  22430  volun  22577  mbfmulc2lem  22682  mbfaddlem  22695  0pledm  22710  i1faddlem  22730  i1fmullem  22731  i1fadd  22732  i1fmul  22733  itg1addlem4  22736  i1fmulclem  22739  i1fmulc  22740  itg1lea  22749  itg1le  22750  mbfi1fseqlem5  22756  mbfi1flimlem  22759  mbfmullem2  22761  xrge0f  22768  itg2ge0  22772  itg2lea  22781  itg2mulclem  22783  itg2mulc  22784  itg2splitlem  22785  itg2split  22786  itg2monolem1  22787  itg2mono  22790  itg2i1fseqle  22791  itg2i1fseq  22792  itg2addlem  22795  itg2cnlem1  22798  dvaddf  22975  dvmulf  22976  dvcmulf  22978  dv11cn  23032  plyaddlem1  23246  plyaddlem  23248  coeeulem  23257  coeaddlem  23282  coemulc  23288  dgradd2  23301  dgrcolem2  23307  ofmulrt  23314  plydivlem3  23327  plydivlem4  23328  plydiveu  23330  plyrem  23337  vieta1lem2  23343  elqaalem3  23353  elqaalem3OLD  23356  qaa  23358  jensenlem2  23992  jensen  23993  basellem7  24092  basellem9  24094  dchrmulcl  24256  chssoc  27230  chjidm  27254  mdslmd3i  28066  inin  28228  disjnf  28258  ofrn  28316  ofrn2  28317  ofresid  28319  gsumle  28616  hauseqcn  28775  ofcof  29002  carsgclctunlem1  29222  carsgclctun  29226  sibfof  29246  ofccat  29501  plymul02  29507  signshf  29549  msrid  30255  nepss  30422  bj-inrab2  31599  poimirlem1  32005  poimirlem2  32006  poimirlem3  32007  poimirlem4  32008  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem10  32014  poimirlem11  32015  poimirlem12  32016  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem23  32027  poimirlem24  32028  poimirlem25  32029  poimirlem28  32032  poimirlem29  32033  poimirlem30  32034  poimirlem31  32035  poimirlem32  32036  broucube  32038  itg2addnclem  32057  itg2addnclem3  32059  itg2addnc  32060  ftc1anclem3  32083  ftc1anclem5  32085  ftc1anclem6  32086  ftc1anclem8  32088  blbnd  32183  lshpinN  32626  lfladdcl  32708  lflvscl  32714  ldualvaddval  32768  lclkrlem2e  35150  mzpclall  35640  mzpindd  35659  dgrsub2  36065  mpaaeu  36087  mendring  36129  corclrcl  36370  relexpaddss  36381  caofcan  36742  ofmul12  36744  ofdivrec  36745  ofdivcan4  36746  ofdivdiv2  36747  expgrowth  36754  binomcxplemrat  36769  binomcxplemnotnn0  36775  disjf1  37528  dvsinax  37880  dvcosax  37895  dvdivcncf  37896  meadjun  38416  uzlidlring  40437  ofaddmndmap  40633  mndpsuppss  40664  mndpfsupp  40669  dmatALTbas  40702  dflinc2  40711  fdivmpt  40859  aacllem  41046