MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inidm Unicode version

Theorem inidm 3542
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.
StepHypRef Expression
1 anidm 626 . 2  |-  ( ( x  e.  A  /\  x  e.  A )  <->  x  e.  A )
21ineqri 3526 1  |-  ( A  i^i  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725    i^i cin 3311
This theorem is referenced by:  inindi  3550  inindir  3551  uneqin  3584  ssdifeq0  3702  intsng  4077  xpindi  4999  xpindir  5000  fnfvof  6308  ofres  6312  offval2  6313  ofrfval2  6314  ofco  6315  offveq  6316  offveqb  6317  ofc1  6318  ofc2  6319  caofref  6321  caofrss  6328  caoftrn  6330  suppssof1  6337  fisn  7423  dffi3  7427  ofsubeq0  9986  ofnegsub  9987  ofsubge0  9988  seqof  11368  incexc  12605  sadeq  12972  smuval2  12982  smumul  12993  ressinbas  13513  pwsle  13702  pwsleval  13703  ghmplusg  15449  gsumzaddlem  15514  gsumzadd  15515  crng2idl  16298  psrbaglesupp  16421  psrbagaddcl  16423  psrbagcon  16424  psrbaglefi  16425  psrbagconf1o  16427  gsumbagdiaglem  16428  psraddcl  16435  psrvscacl  16445  psrlidm  16455  psrdi  16458  psrdir  16459  mplsubglem  16486  psrbagev1  16554  psrplusgpropd  16617  coe1add  16645  baspartn  17007  indistopon  17053  epttop  17061  ptbasin  17597  snfil  17884  tsmsadd  18164  ust0  18237  ustuqtop1  18259  volun  19427  mbfmulc2lem  19527  mbfaddlem  19540  0pledm  19553  i1faddlem  19573  i1fmullem  19574  i1fadd  19575  i1fmul  19576  itg1addlem4  19579  i1fmulclem  19582  i1fmulc  19583  itg1lea  19592  itg1le  19593  mbfi1fseqlem5  19599  mbfi1flimlem  19602  mbfmullem2  19604  xrge0f  19611  itg2ge0  19615  itg2lea  19624  itg2mulclem  19626  itg2mulc  19627  itg2splitlem  19628  itg2split  19629  itg2monolem1  19630  itg2mono  19633  itg2i1fseqle  19634  itg2i1fseq  19635  itg2addlem  19638  itg2cnlem1  19641  dvaddf  19816  dvmulf  19817  dvcmulf  19819  dv11cn  19873  evlslem3  19923  evlslem1  19924  pf1ind  19963  plyaddlem1  20120  plyaddlem  20122  coeeulem  20131  coeaddlem  20155  coemulc  20161  dgradd2  20174  dgrcolem2  20180  ofmulrt  20187  plydivlem3  20200  plydivlem4  20201  plydiveu  20203  plyrem  20210  vieta1lem2  20216  elqaalem3  20226  qaa  20228  jensenlem2  20814  jensen  20815  basellem7  20857  basellem9  20859  dchrmulcl  21021  chssoc  22986  chjidm  23010  mdslmd3i  23823  inin  23984  ofrn  24040  ofrn2  24041  ofresid  24043  offval2f  24068  hauseqcn  24281  sibfof  24642  nepss  25163  predidm  25443  itg2addnclem  26202  itg2addnclem3  26204  itg2addnc  26205  blbnd  26433  lcomf  26683  mzpclall  26721  mzpindd  26740  frlmsslsp  27163  frlmup1  27165  dgrsub2  27254  mpaaeu  27270  mndvcl  27361  mendrng  27415  caofcan  27455  ofmul12  27457  ofdivrec  27458  ofdivcan4  27459  ofdivdiv2  27460  expgrowth  27467  lshpinN  29626  lfladdcl  29708  lflvscl  29714  ldualvaddval  29768  lclkrlem2e  32148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319
  Copyright terms: Public domain W3C validator