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

Theorem inidm 3391
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 3375 1  |-  ( A  i^i  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696    i^i cin 3164
This theorem is referenced by:  inindi  3399  inindir  3400  uneqin  3433  ssdifeq0  3549  intsng  3913  xpindi  4835  xpindir  4836  fnfvof  6106  ofres  6110  offval2  6111  ofrfval2  6112  ofco  6113  offveq  6114  offveqb  6115  ofc1  6116  ofc2  6117  caofref  6119  caofrss  6126  caoftrn  6128  suppssof1  6135  fisn  7196  dffi3  7200  ofsubeq0  9759  ofnegsub  9760  ofsubge0  9761  seqof  11119  incexc  12312  sadeq  12679  smuval2  12689  smumul  12700  ressinbas  13220  pwsle  13407  pwsleval  13408  ghmplusg  15154  gsumzaddlem  15219  gsumzadd  15220  crng2idl  16007  psrbaglesupp  16130  psrbagaddcl  16132  psrbagcon  16133  psrbaglefi  16134  psrbagconf1o  16136  gsumbagdiaglem  16137  psraddcl  16144  psrvscacl  16154  psrlidm  16164  psrdi  16167  psrdir  16168  mplsubglem  16195  psrbagev1  16263  psrplusgpropd  16329  coe1add  16357  baspartn  16708  indistopon  16754  epttop  16762  ptbasin  17288  snfil  17575  tsmsadd  17845  volun  18918  mbfmulc2lem  19018  mbfaddlem  19031  0pledm  19044  i1faddlem  19064  i1fmullem  19065  i1fadd  19066  i1fmul  19067  itg1addlem4  19070  i1fmulclem  19073  i1fmulc  19074  itg1lea  19083  itg1le  19084  mbfi1fseqlem5  19090  mbfi1flimlem  19093  mbfmullem2  19095  xrge0f  19102  itg2ge0  19106  itg2lea  19115  itg2mulclem  19117  itg2mulc  19118  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2addlem  19129  itg2cnlem1  19132  dvaddf  19307  dvmulf  19308  dvcmulf  19310  dv11cn  19364  evlslem3  19414  evlslem1  19415  pf1ind  19454  plyaddlem1  19611  plyaddlem  19613  coeeulem  19622  coeaddlem  19646  coemulc  19652  dgradd2  19665  dgrcolem2  19671  ofmulrt  19678  plydivlem3  19691  plydivlem4  19692  plydiveu  19694  plyrem  19701  vieta1lem2  19707  elqaalem3  19717  qaa  19719  jensenlem2  20298  jensen  20299  basellem7  20340  basellem9  20342  dchrmulcl  20504  chssoc  22091  chjidm  22115  mdslmd3i  22928  inin  23183  ofrn  23221  ofrn2  23222  offval2f  23248  nepss  24087  predidm  24259  itg2addnclem  25003  itg2addnc  25005  empos  25345  dispos  25390  hdrmp  25809  indcls2  26099  blbnd  26614  lcomf  26870  mzpclall  26908  mzpindd  26927  frlmsslsp  27351  frlmup1  27353  dgrsub2  27442  mpaaeu  27458  mndvcl  27549  mendrng  27603  caofcan  27643  ofmul12  27645  ofdivrec  27646  ofdivcan4  27647  ofdivdiv2  27648  expgrowth  27655  lshpinN  29801  lfladdcl  29883  lflvscl  29889  ldualvaddval  29943  lclkrlem2e  32323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator