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

Theorem inidm 4179
Description: Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
inidm (𝐴𝐴) = 𝐴

Proof of Theorem inidm
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 anidm 566 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21ineqri 4165 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  cin 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918
This theorem is referenced by:  inindi  4187  inindir  4188  uneqin  4239  disjeq0  4416  ssdifeq0  4445  intsng  4947  xpindi  5790  xpindir  5791  resindm  5987  elidinxpid  5999  idinxpresid  6002  predidm  6281  offval2f  7633  fnfvof  7635  ofres  7637  offval2  7638  ofrfval2  7639  ofco  7641  offveq  7642  offveqb  7643  ofc1  7644  ofc2  7645  caofref  7647  caofrss  7654  caoftrn  7656  offsplitfpar  8052  suppssof1  8131  suppofssd  8135  suppofss1d  8136  suppofss2d  8137  fisn  9364  dffi3  9368  ofsubeq0  12151  ofnegsub  12152  ofsubge0  12153  seqof  13966  ofccat  14855  incexc  15723  sadeq  16353  smuval2  16363  smumul  16374  ressinbas  17127  pwsle  17375  pwsleval  17376  ghmplusg  19625  gsumzaddlem  19699  gsumzadd  19700  pwspjmhmmgpd  20044  lcomf  20364  crng2idl  20712  frlmipval  21188  frlmphllem  21189  frlmphl  21190  frlmsslsp  21205  frlmup1  21207  psrbaglesupp  21329  psrbaglesuppOLD  21330  psrbagaddcl  21333  psrbagaddclOLD  21334  psrbagcon  21335  psrbagconOLD  21336  psrbaglefi  21337  psrbaglefiOLD  21338  psrbagconf1o  21341  psrbagconf1oOLD  21342  gsumbagdiaglemOLD  21343  gsumbagdiaglem  21346  psraddcl  21354  psrvscacl  21364  psrlidm  21375  psrdi  21378  psrdir  21379  mplsubglem  21408  psrbagev1  21488  psrbagev1OLD  21489  evlslem3  21493  evlslem1  21495  mhpmulcl  21542  psrplusgpropd  21610  coe1add  21638  pf1ind  21724  mndvcl  21743  matplusgcell  21785  matsubgcell  21786  mat1dimscm  21827  baspartn  22307  indistopon  22354  epttop  22362  dissnlocfin  22883  ptbasin  22931  snfil  23218  tsmsadd  23501  ust0  23574  ustuqtop1  23596  rrxcph  24759  rrxds  24760  volun  24912  mbfmulc2lem  25014  mbfaddlem  25027  0pledm  25040  i1faddlem  25060  i1fmullem  25061  i1fadd  25062  i1fmul  25063  itg1addlem4  25066  itg1addlem4OLD  25067  i1fmulclem  25070  i1fmulc  25071  itg1lea  25080  itg1le  25081  mbfi1fseqlem5  25087  mbfi1flimlem  25090  mbfmullem2  25092  xrge0f  25099  itg2ge0  25103  itg2lea  25112  itg2mulclem  25114  itg2mulc  25115  itg2splitlem  25116  itg2split  25117  itg2monolem1  25118  itg2mono  25121  itg2i1fseqle  25122  itg2i1fseq  25123  itg2addlem  25126  itg2cnlem1  25129  dvaddf  25309  dvmulf  25310  dvcmulf  25312  dv11cn  25368  plyaddlem1  25577  plyaddlem  25579  coeeulem  25588  coeaddlem  25613  coemulc  25619  dgradd2  25632  dgrcolem2  25638  ofmulrt  25645  plydivlem3  25658  plydivlem4  25659  plydiveu  25661  plyrem  25668  vieta1lem2  25674  elqaalem3  25684  qaa  25686  jensenlem2  26340  jensen  26341  basellem7  26439  basellem9  26441  dchrmulcl  26600  chssoc  30441  chjidm  30465  mdslmd3i  31277  inin  31445  unidifsnne  31466  disjnf  31491  ofrn  31558  ofrn2  31559  ofresid  31561  offinsupp1  31647  gsumle  31935  tocyccntz  31996  islinds5  32159  ellspds  32160  evls1fpws  32274  fedgmullem1  32327  hauseqcn  32482  ofcof  32709  carsgclctunlem1  32920  carsgclctun  32924  sibfof  32943  plymul02  33161  signshf  33203  circlemethhgt  33259  msrid  34142  nepss  34292  bj-inrab2  35401  matunitlindflem1  36077  matunitlindflem2  36078  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem4  36085  poimirlem6  36087  poimirlem7  36088  poimirlem8  36089  poimirlem10  36091  poimirlem11  36092  poimirlem12  36093  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem23  36104  poimirlem24  36105  poimirlem25  36106  poimirlem28  36109  poimirlem29  36110  poimirlem30  36111  poimirlem31  36112  poimirlem32  36113  broucube  36115  itg2addnclem  36132  itg2addnclem3  36134  itg2addnc  36135  ftc1anclem3  36156  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem8  36161  blbnd  36249  lshpinN  37454  lfladdcl  37536  lflvscl  37542  ldualvaddval  37596  lclkrlem2e  39977  ofun  40663  evlsbagval  40751  fsuppind  40768  fsuppssind  40771  mhphf  40774  mzpclall  41053  mzpindd  41072  dgrsub2  41465  mpaaeu  41480  mendring  41522  ofoafo  41673  ofoacl  41674  ofoaid1  41675  ofoaid2  41676  ofoaass  41677  ofoacom  41678  naddcnff  41679  naddcnffo  41681  naddcnfcom  41683  naddcnfid1  41684  naddcnfass  41686  relexpaddss  41997  ntrkbimka  42317  clsk3nimkb  42319  caofcan  42610  ofmul12  42612  ofdivrec  42613  ofdivcan4  42614  ofdivdiv2  42615  expgrowth  42622  binomcxplemrat  42637  binomcxplemnotnn0  42643  disjf1  43408  dvsinax  44161  dvcosax  44174  dvdivcncf  44175  meadjun  44710  smfmulc1  45044  f1cof1blem  45315  uzlidlring  46234  ofaddmndmap  46426  mndpsuppss  46454  dmatALTbas  46489  dflinc2  46498  fdivmpt  46633  aacllem  47255  amgmwlem  47256
  Copyright terms: Public domain W3C validator