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

Theorem inidm 3285
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
StepHypRef Expression
1 anidm 628 . 2  |-  ( ( x  e.  A  /\  x  e.  A )  <->  x  e.  A )
21ineqri 3270 1  |-  ( A  i^i  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621    i^i cin 3077
This theorem is referenced by:  inindi  3293  inindir  3294  uneqin  3327  ssdifeq0  3442  intsng  3795  xpindi  4726  xpindir  4727  fnfvof  5942  ofres  5946  offval2  5947  ofrfval2  5948  ofco  5949  offveq  5950  offveqb  5951  ofc1  5952  ofc2  5953  caofref  5955  caofrss  5962  caoftrn  5964  suppssof1  5971  fisn  7064  dffi3  7068  ofsubeq0  9623  ofnegsub  9624  ofsubge0  9625  seqof  10981  sadeq  12537  smuval2  12547  smumul  12558  ressinbas  13078  pwsle  13265  pwsleval  13266  ghmplusg  14973  gsumzaddlem  15038  gsumzadd  15039  crng2idl  15823  psrbaglesupp  15946  psrbagaddcl  15948  psrbagcon  15949  psrbaglefi  15950  psrbagconf1o  15952  gsumbagdiaglem  15953  psraddcl  15960  psrvscacl  15970  psrlidm  15980  psrdi  15983  psrdir  15984  mplsubglem  16011  psrbagev1  16079  psrplusgpropd  16145  coe1add  16173  baspartn  16524  indistopon  16570  epttop  16578  ptbasin  17104  snfil  17391  tsmsadd  17661  volun  18734  mbfmulc2lem  18834  mbfaddlem  18847  0pledm  18860  i1faddlem  18880  i1fmullem  18881  i1fadd  18882  i1fmul  18883  itg1addlem4  18886  i1fmulclem  18889  i1fmulc  18890  itg1lea  18899  itg1le  18900  mbfi1fseqlem5  18906  mbfi1flimlem  18909  mbfmullem2  18911  xrge0f  18918  itg2ge0  18922  itg2lea  18931  itg2mulclem  18933  itg2mulc  18934  itg2splitlem  18935  itg2split  18936  itg2monolem1  18937  itg2mono  18940  itg2i1fseqle  18941  itg2i1fseq  18942  itg2addlem  18945  itg2cnlem1  18948  dvaddf  19123  dvmulf  19124  dvcmulf  19126  dv11cn  19180  evlslem3  19230  evlslem1  19231  pf1ind  19270  plyaddlem1  19427  plyaddlem  19429  coeeulem  19438  coeaddlem  19462  coemulc  19468  dgradd2  19481  dgrcolem2  19487  ofmulrt  19494  plydivlem3  19507  plydivlem4  19508  plydiveu  19510  plyrem  19517  vieta1lem2  19523  elqaalem3  19533  qaa  19535  jensenlem2  20114  jensen  20115  basellem7  20156  basellem9  20158  dchrmulcl  20320  chssoc  21905  chjidm  21929  mdslmd3i  22742  nepss  23243  predidm  23356  empos  24408  dispos  24453  hdrmp  24872  indcls2  25162  blbnd  25677  lcomf  25933  mzpclall  25971  mzpindd  25990  frlmsslsp  26414  frlmup1  26416  dgrsub2  26505  mpaaeu  26521  mndvcl  26612  mendrng  26666  caofcan  26706  ofmul12  26708  ofdivrec  26709  ofdivcan4  26710  ofdivdiv2  26711  expgrowth  26718  lshpinN  27868  lfladdcl  27950  lflvscl  27956  ldualvaddval  28010  lclkrlem2e  30390
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085
  Copyright terms: Public domain W3C validator