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

Theorem inidm 3855
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 677 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21ineqri 3839 1 (𝐴𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614
This theorem is referenced by:  inindi  3863  inindir  3864  uneqin  3911  ssdifeq0  4084  intsng  4544  xpindi  5288  xpindir  5289  resindm  5479  predidm  5740  offval2f  6951  fnfvof  6953  ofres  6955  offval2  6956  ofrfval2  6957  ofco  6959  offveq  6960  offveqb  6961  ofc1  6962  ofc2  6963  caofref  6965  caofrss  6972  caoftrn  6974  suppssof1  7373  suppofss1d  7377  suppofss2d  7378  fisn  8374  dffi3  8378  ofsubeq0  11055  ofnegsub  11056  ofsubge0  11057  seqof  12898  ofccat  13754  incexc  14613  sadeq  15241  smuval2  15251  smumul  15262  ressinbas  15983  pwsle  16199  pwsleval  16200  ghmplusg  18295  gsumzaddlem  18367  gsumzadd  18368  lcomf  18950  lcomfsupp  18951  crng2idl  19287  psrbaglesupp  19416  psrbagaddcl  19418  psrbagcon  19419  psrbaglefi  19420  psrbagconf1o  19422  gsumbagdiaglem  19423  psraddcl  19431  psrvscacl  19441  psrlidm  19451  psrdi  19454  psrdir  19455  mplsubglem  19482  psrbagev1  19558  evlslem3  19562  evlslem1  19563  psrplusgpropd  19654  coe1add  19682  pf1ind  19767  frlmipval  20166  frlmphllem  20167  frlmphl  20168  frlmsslsp  20183  frlmup1  20185  mndvcl  20245  matplusgcell  20287  matsubgcell  20288  mat1dimscm  20329  baspartn  20806  indistopon  20853  epttop  20861  dissnlocfin  21380  ptbasin  21428  snfil  21715  tsmsadd  21997  ust0  22070  ustuqtop1  22092  rrxcph  23226  rrxds  23227  volun  23359  mbfmulc2lem  23459  mbfaddlem  23472  0pledm  23485  i1faddlem  23505  i1fmullem  23506  i1fadd  23507  i1fmul  23508  itg1addlem4  23511  i1fmulclem  23514  i1fmulc  23515  itg1lea  23524  itg1le  23525  mbfi1fseqlem5  23531  mbfi1flimlem  23534  mbfmullem2  23536  xrge0f  23543  itg2ge0  23547  itg2lea  23556  itg2mulclem  23558  itg2mulc  23559  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2mono  23565  itg2i1fseqle  23566  itg2i1fseq  23567  itg2addlem  23570  itg2cnlem1  23573  dvaddf  23750  dvmulf  23751  dvcmulf  23753  dv11cn  23809  plyaddlem1  24014  plyaddlem  24016  coeeulem  24025  coeaddlem  24050  coemulc  24056  dgradd2  24069  dgrcolem2  24075  ofmulrt  24082  plydivlem3  24095  plydivlem4  24096  plydiveu  24098  plyrem  24105  vieta1lem2  24111  elqaalem3  24121  qaa  24123  jensenlem2  24759  jensen  24760  basellem7  24858  basellem9  24860  dchrmulcl  25019  chssoc  28483  chjidm  28507  mdslmd3i  29319  inin  29478  disjnf  29510  ofrn  29569  ofrn2  29570  ofresid  29572  gsumle  29907  hauseqcn  30069  ofcof  30297  carsgclctunlem1  30507  carsgclctun  30511  sibfof  30530  plymul02  30751  signshf  30793  circlemethhgt  30849  msrid  31568  nepss  31725  bj-inrab2  33049  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem28  33567  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  broucube  33573  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  ftc1anclem3  33617  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem8  33622  blbnd  33716  lshpinN  34594  lfladdcl  34676  lflvscl  34682  ldualvaddval  34736  lclkrlem2e  37117  mzpclall  37607  mzpindd  37626  dgrsub2  38022  mpaaeu  38037  mendring  38079  corclrcl  38316  relexpaddss  38327  ntrkbimka  38653  clsk3nimkb  38655  caofcan  38839  ofmul12  38841  ofdivrec  38842  ofdivcan4  38843  ofdivdiv2  38844  expgrowth  38851  binomcxplemrat  38866  binomcxplemnotnn0  38872  disjf1  39683  dvsinax  40445  dvcosax  40459  dvdivcncf  40460  meadjun  40997  smfmulc1  41324  uzlidlring  42254  ofaddmndmap  42447  mndpsuppss  42477  mndpfsupp  42482  dmatALTbas  42515  dflinc2  42524  fdivmpt  42659  aacllem  42875  amgmwlem  42876
  Copyright terms: Public domain W3C validator