Theorem inidm 3641

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.

Step	Hyp	Ref	Expression
1		anidm 650	. 2 |- ( ( x e. A /\ x e. A ) <-> x e. A )
2	1	ineqri 3626	1 |- ( A i^i A ) = A

Syntax hints:   = wceq 1444   e. wcel 1887   i^i cin 3403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411

This theorem is referenced by:  inindi  3649  inindir  3650  uneqin  3694  ssdifeq0  3850  intsng  4270  xpindi  4968  xpindir  4969  resindm  5149  predidm  5402  offval2f  6543  fnfvof  6545  ofres  6547  offval2  6548  ofrfval2  6549  ofco  6551  offveq  6552  offveqb  6553  ofc1  6554  ofc2  6555  caofref  6557  caofrss  6564  caoftrn  6566  suppssof1  6948  suppofss1d  6952  suppofss2d  6953  fisn  7941  dffi3  7945  ofsubeq0  10606  ofnegsub  10607  ofsubge0  10608  seqof  12270  incexc  13895  sadeq  14446  smuval2  14456  smumul  14467  ressinbas  15185  pwsle  15390  pwsleval  15391  ghmplusg  17484  gsumzaddlem  17554  gsumzadd  17555  lcomf  18127  lcomfsupp  18128  crng2idl  18463  psrbaglesupp  18592  psrbagaddcl  18594  psrbagcon  18595  psrbaglefi  18596  psrbagconf1o  18598  gsumbagdiaglem  18599  psraddcl  18607  psrvscacl  18617  psrlidm  18627  psrdi  18630  psrdir  18631  mplsubglem  18658  psrbagev1  18733  evlslem3  18737  evlslem1  18738  psrplusgpropd  18829  coe1add  18857  pf1ind  18943  frlmipval  19337  frlmphllem  19338  frlmphl  19339  frlmsslsp  19354  frlmup1  19356  mndvcl  19416  matplusgcell  19458  matsubgcell  19459  mat1dimscm  19500  baspartn  19969  indistopon  20016  epttop  20024  dissnlocfin  20544  ptbasin  20592  snfil  20879  tsmsadd  21161  ust0  21234  ustuqtop1  21256  rrxcph  22351  rrxds  22352  volun  22498  mbfmulc2lem  22603  mbfaddlem  22616  0pledm  22631  i1faddlem  22651  i1fmullem  22652  i1fadd  22653  i1fmul  22654  itg1addlem4  22657  i1fmulclem  22660  i1fmulc  22661  itg1lea  22670  itg1le  22671  mbfi1fseqlem5  22677  mbfi1flimlem  22680  mbfmullem2  22682  xrge0f  22689  itg2ge0  22693  itg2lea  22702  itg2mulclem  22704  itg2mulc  22705  itg2splitlem  22706  itg2split  22707  itg2monolem1  22708  itg2mono  22711  itg2i1fseqle  22712  itg2i1fseq  22713  itg2addlem  22716  itg2cnlem1  22719  dvaddf  22896  dvmulf  22897  dvcmulf  22899  dv11cn  22953  plyaddlem1  23167  plyaddlem  23169  coeeulem  23178  coeaddlem  23203  coemulc  23209  dgradd2  23222  dgrcolem2  23228  ofmulrt  23235  plydivlem3  23248  plydivlem4  23249  plydiveu  23251  plyrem  23258  vieta1lem2  23264  elqaalem3  23274  elqaalem3OLD  23277  qaa  23279  jensenlem2  23913  jensen  23914  basellem7  24013  basellem9  24015  dchrmulcl  24177  chssoc  27149  chjidm  27173  mdslmd3i  27985  inin  28149  disjnf  28181  ofrn  28240  ofrn2  28241  ofresid  28243  gsumle  28542  hauseqcn  28701  ofcof  28928  carsgclctunlem1  29149  carsgclctun  29153  sibfof  29173  ofccat  29429  plymul02  29435  signshf  29477  msrid  30183  nepss  30350  bj-inrab2  31531  poimirlem1  31941  poimirlem2  31942  poimirlem3  31943  poimirlem4  31944  poimirlem6  31946  poimirlem7  31947  poimirlem8  31948  poimirlem10  31950  poimirlem11  31951  poimirlem12  31952  poimirlem16  31956  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem23  31963  poimirlem24  31964  poimirlem25  31965  poimirlem28  31968  poimirlem29  31969  poimirlem30  31970  poimirlem31  31971  poimirlem32  31972  broucube  31974  itg2addnclem  31993  itg2addnclem3  31995  itg2addnc  31996  ftc1anclem3  32019  ftc1anclem5  32021  ftc1anclem6  32022  ftc1anclem8  32024  blbnd  32119  lshpinN  32555  lfladdcl  32637  lflvscl  32643  ldualvaddval  32697  lclkrlem2e  35079  mzpclall  35569  mzpindd  35588  dgrsub2  35994  mpaaeu  36016  mendring  36058  corclrcl  36299  relexpaddss  36310  caofcan  36672  ofmul12  36674  ofdivrec  36675  ofdivcan4  36676  ofdivdiv2  36677  expgrowth  36684  binomcxplemrat  36699  binomcxplemnotnn0  36705  disjf1  37457  dvsinax  37783  dvcosax  37798  dvdivcncf  37799  meadjun  38300  uzlidlring  39982  ofaddmndmap  40178  mndpsuppss  40209  mndpfsupp  40214  dmatALTbas  40247  dflinc2  40256  fdivmpt  40404  aacllem  40593