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

Theorem inidm 3378
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 625 . 2  |-  ( ( x  e.  A  /\  x  e.  A )  <->  x  e.  A )
21ineqri 3362 1  |-  ( A  i^i  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684    i^i cin 3151
This theorem is referenced by:  inindi  3386  inindir  3387  uneqin  3420  ssdifeq0  3536  intsng  3897  xpindi  4819  xpindir  4820  fnfvof  6090  ofres  6094  offval2  6095  ofrfval2  6096  ofco  6097  offveq  6098  offveqb  6099  ofc1  6100  ofc2  6101  caofref  6103  caofrss  6110  caoftrn  6112  suppssof1  6119  fisn  7180  dffi3  7184  ofsubeq0  9743  ofnegsub  9744  ofsubge0  9745  seqof  11103  incexc  12296  sadeq  12663  smuval2  12673  smumul  12684  ressinbas  13204  pwsle  13391  pwsleval  13392  ghmplusg  15138  gsumzaddlem  15203  gsumzadd  15204  crng2idl  15991  psrbaglesupp  16114  psrbagaddcl  16116  psrbagcon  16117  psrbaglefi  16118  psrbagconf1o  16120  gsumbagdiaglem  16121  psraddcl  16128  psrvscacl  16138  psrlidm  16148  psrdi  16151  psrdir  16152  mplsubglem  16179  psrbagev1  16247  psrplusgpropd  16313  coe1add  16341  baspartn  16692  indistopon  16738  epttop  16746  ptbasin  17272  snfil  17559  tsmsadd  17829  volun  18902  mbfmulc2lem  19002  mbfaddlem  19015  0pledm  19028  i1faddlem  19048  i1fmullem  19049  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  i1fmulclem  19057  i1fmulc  19058  itg1lea  19067  itg1le  19068  mbfi1fseqlem5  19074  mbfi1flimlem  19077  mbfmullem2  19079  xrge0f  19086  itg2ge0  19090  itg2lea  19099  itg2mulclem  19101  itg2mulc  19102  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2addlem  19113  itg2cnlem1  19116  dvaddf  19291  dvmulf  19292  dvcmulf  19294  dv11cn  19348  evlslem3  19398  evlslem1  19399  pf1ind  19438  plyaddlem1  19595  plyaddlem  19597  coeeulem  19606  coeaddlem  19630  coemulc  19636  dgradd2  19649  dgrcolem2  19655  ofmulrt  19662  plydivlem3  19675  plydivlem4  19676  plydiveu  19678  plyrem  19685  vieta1lem2  19691  elqaalem3  19701  qaa  19703  jensenlem2  20282  jensen  20283  basellem7  20324  basellem9  20326  dchrmulcl  20488  chssoc  22075  chjidm  22099  mdslmd3i  22912  inin  23167  ofrn  23206  ofrn2  23207  offval2f  23233  nepss  24072  predidm  24188  empos  25242  dispos  25287  hdrmp  25706  indcls2  25996  blbnd  26511  lcomf  26767  mzpclall  26805  mzpindd  26824  frlmsslsp  27248  frlmup1  27250  dgrsub2  27339  mpaaeu  27355  mndvcl  27446  mendrng  27500  caofcan  27540  ofmul12  27542  ofdivrec  27543  ofdivcan4  27544  ofdivdiv2  27545  expgrowth  27552  lshpinN  29179  lfladdcl  29261  lflvscl  29267  ldualvaddval  29321  lclkrlem2e  31701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator