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

Theorem inidm 3339
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 3323 1  |-  ( A  i^i  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621    i^i cin 3112
This theorem is referenced by:  inindi  3347  inindir  3348  uneqin  3381  ssdifeq0  3497  intsng  3857  xpindi  4793  xpindir  4794  fnfvof  6010  ofres  6014  offval2  6015  ofrfval2  6016  ofco  6017  offveq  6018  offveqb  6019  ofc1  6020  ofc2  6021  caofref  6023  caofrss  6030  caoftrn  6032  suppssof1  6039  fisn  7134  dffi3  7138  ofsubeq0  9697  ofnegsub  9698  ofsubge0  9699  seqof  11055  sadeq  12611  smuval2  12621  smumul  12632  ressinbas  13152  pwsle  13339  pwsleval  13340  ghmplusg  15086  gsumzaddlem  15151  gsumzadd  15152  crng2idl  15939  psrbaglesupp  16062  psrbagaddcl  16064  psrbagcon  16065  psrbaglefi  16066  psrbagconf1o  16068  gsumbagdiaglem  16069  psraddcl  16076  psrvscacl  16086  psrlidm  16096  psrdi  16099  psrdir  16100  mplsubglem  16127  psrbagev1  16195  psrplusgpropd  16261  coe1add  16289  baspartn  16640  indistopon  16686  epttop  16694  ptbasin  17220  snfil  17507  tsmsadd  17777  volun  18850  mbfmulc2lem  18950  mbfaddlem  18963  0pledm  18976  i1faddlem  18996  i1fmullem  18997  i1fadd  18998  i1fmul  18999  itg1addlem4  19002  i1fmulclem  19005  i1fmulc  19006  itg1lea  19015  itg1le  19016  mbfi1fseqlem5  19022  mbfi1flimlem  19025  mbfmullem2  19027  xrge0f  19034  itg2ge0  19038  itg2lea  19047  itg2mulclem  19049  itg2mulc  19050  itg2splitlem  19051  itg2split  19052  itg2monolem1  19053  itg2mono  19056  itg2i1fseqle  19057  itg2i1fseq  19058  itg2addlem  19061  itg2cnlem1  19064  dvaddf  19239  dvmulf  19240  dvcmulf  19242  dv11cn  19296  evlslem3  19346  evlslem1  19347  pf1ind  19386  plyaddlem1  19543  plyaddlem  19545  coeeulem  19554  coeaddlem  19578  coemulc  19584  dgradd2  19597  dgrcolem2  19603  ofmulrt  19610  plydivlem3  19623  plydivlem4  19624  plydiveu  19626  plyrem  19633  vieta1lem2  19639  elqaalem3  19649  qaa  19651  jensenlem2  20230  jensen  20231  basellem7  20272  basellem9  20274  dchrmulcl  20436  chssoc  22021  chjidm  22045  mdslmd3i  22858  nepss  23430  predidm  23543  empos  24595  dispos  24640  hdrmp  25059  indcls2  25349  blbnd  25864  lcomf  26120  mzpclall  26158  mzpindd  26177  frlmsslsp  26601  frlmup1  26603  dgrsub2  26692  mpaaeu  26708  mndvcl  26799  mendrng  26853  caofcan  26893  ofmul12  26895  ofdivrec  26896  ofdivcan4  26897  ofdivdiv2  26898  expgrowth  26905  lshpinN  28330  lfladdcl  28412  lflvscl  28418  ldualvaddval  28472  lclkrlem2e  30852
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-in 3120
  Copyright terms: Public domain W3C validator