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

Theorem inidm 3379
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
Dummy variable  x is distinct from all other variables.

Proof of Theorem inidm
StepHypRef Expression
1 anidm 627 . 2  |-  ( ( x  e.  A  /\  x  e.  A )  <->  x  e.  A )
21ineqri 3363 1  |-  ( A  i^i  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1624    e. wcel 1685    i^i cin 3152
This theorem is referenced by:  inindi  3387  inindir  3388  uneqin  3421  ssdifeq0  3537  intsng  3898  xpindi  4818  xpindir  4819  fnfvof  6051  ofres  6055  offval2  6056  ofrfval2  6057  ofco  6058  offveq  6059  offveqb  6060  ofc1  6061  ofc2  6062  caofref  6064  caofrss  6071  caoftrn  6073  suppssof1  6080  fisn  7175  dffi3  7179  ofsubeq0  9738  ofnegsub  9739  ofsubge0  9740  seqof  11097  incexc  12290  sadeq  12657  smuval2  12667  smumul  12678  ressinbas  13198  pwsle  13385  pwsleval  13386  ghmplusg  15132  gsumzaddlem  15197  gsumzadd  15198  crng2idl  15985  psrbaglesupp  16108  psrbagaddcl  16110  psrbagcon  16111  psrbaglefi  16112  psrbagconf1o  16114  gsumbagdiaglem  16115  psraddcl  16122  psrvscacl  16132  psrlidm  16142  psrdi  16145  psrdir  16146  mplsubglem  16173  psrbagev1  16241  psrplusgpropd  16307  coe1add  16335  baspartn  16686  indistopon  16732  epttop  16740  ptbasin  17266  snfil  17553  tsmsadd  17823  volun  18896  mbfmulc2lem  18996  mbfaddlem  19009  0pledm  19022  i1faddlem  19042  i1fmullem  19043  i1fadd  19044  i1fmul  19045  itg1addlem4  19048  i1fmulclem  19051  i1fmulc  19052  itg1lea  19061  itg1le  19062  mbfi1fseqlem5  19068  mbfi1flimlem  19071  mbfmullem2  19073  xrge0f  19080  itg2ge0  19084  itg2lea  19093  itg2mulclem  19095  itg2mulc  19096  itg2splitlem  19097  itg2split  19098  itg2monolem1  19099  itg2mono  19102  itg2i1fseqle  19103  itg2i1fseq  19104  itg2addlem  19107  itg2cnlem1  19110  dvaddf  19285  dvmulf  19286  dvcmulf  19288  dv11cn  19342  evlslem3  19392  evlslem1  19393  pf1ind  19432  plyaddlem1  19589  plyaddlem  19591  coeeulem  19600  coeaddlem  19624  coemulc  19630  dgradd2  19643  dgrcolem2  19649  ofmulrt  19656  plydivlem3  19669  plydivlem4  19670  plydiveu  19672  plyrem  19679  vieta1lem2  19685  elqaalem3  19695  qaa  19697  jensenlem2  20276  jensen  20277  basellem7  20318  basellem9  20320  dchrmulcl  20482  chssoc  22067  chjidm  22091  mdslmd3i  22904  nepss  23476  predidm  23589  empos  24641  dispos  24686  hdrmp  25105  indcls2  25395  blbnd  25910  lcomf  26166  mzpclall  26204  mzpindd  26223  frlmsslsp  26647  frlmup1  26649  dgrsub2  26738  mpaaeu  26754  mndvcl  26845  mendrng  26899  caofcan  26939  ofmul12  26941  ofdivrec  26942  ofdivcan4  26943  ofdivdiv2  26944  expgrowth  26951  lshpinN  28446  lfladdcl  28528  lflvscl  28534  ldualvaddval  28588  lclkrlem2e  30968
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160
  Copyright terms: Public domain W3C validator