Theorem inidm 3552

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 644	. 2 |- ( ( x e. A /\ x e. A ) <-> x e. A )
2	1	ineqri 3537	1 |- ( A i^i A ) = A

Syntax hints:   = wceq 1369   e. wcel 1756   i^i cin 3320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2968  df-in 3328

This theorem is referenced by:  inindi  3560  inindir  3561  uneqin  3594  ssdifeq0  3754  intsng  4156  xpindi  4965  xpindir  4966  resindm  5144  fnfvof  6328  ofres  6330  offval2  6331  ofrfval2  6332  suppssof1OLD  6334  ofco  6335  offveq  6336  offveqb  6337  ofc1  6338  ofc2  6339  caofref  6341  caofrss  6348  caoftrn  6350  suppssof1  6717  suppofss1d  6721  suppofss2d  6722  fisn  7669  dffi3  7673  ofsubeq0  10311  ofnegsub  10312  ofsubge0  10313  seqof  11855  incexc  13292  sadeq  13660  smuval2  13670  smumul  13681  ressinbas  14226  pwsle  14422  pwsleval  14423  ghmplusg  16317  gsumzaddlem  16397  gsumzadd  16398  gsumzaddlemOLD  16399  gsumzaddOLD  16400  lcomf  16959  lcomfsupp  16961  crng2idl  17295  psrbaglesupp  17409  psrbaglesuppOLD  17410  psrbagaddcl  17412  psrbagaddclOLD  17413  psrbagcon  17414  psrbaglefi  17415  psrbaglefiOLD  17416  psrbagconf1o  17418  gsumbagdiaglem  17419  psraddcl  17428  psrvscacl  17438  psrlidm  17448  psrlidmOLD  17449  psrdi  17453  psrdir  17454  mplsubglem  17484  mplsubglemOLD  17486  psrbagev1  17566  psrbagev1OLD  17567  evlslem3  17572  evlslem1  17573  psrplusgpropd  17661  coe1add  17689  pf1ind  17758  frlmipval  18173  frlmphllem  18174  frlmphl  18175  frlmsslsp  18192  frlmsslspOLD  18193  frlmup1  18195  mndvcl  18260  baspartn  18528  indistopon  18574  epttop  18582  ptbasin  19119  snfil  19406  tsmsadd  19690  ust0  19763  ustuqtop1  19785  rrxcph  20865  rrxds  20866  volun  20995  mbfmulc2lem  21094  mbfaddlem  21107  0pledm  21120  i1faddlem  21140  i1fmullem  21141  i1fadd  21142  i1fmul  21143  itg1addlem4  21146  i1fmulclem  21149  i1fmulc  21150  itg1lea  21159  itg1le  21160  mbfi1fseqlem5  21166  mbfi1flimlem  21169  mbfmullem2  21171  xrge0f  21178  itg2ge0  21182  itg2lea  21191  itg2mulclem  21193  itg2mulc  21194  itg2splitlem  21195  itg2split  21196  itg2monolem1  21197  itg2mono  21200  itg2i1fseqle  21201  itg2i1fseq  21202  itg2addlem  21205  itg2cnlem1  21208  dvaddf  21385  dvmulf  21386  dvcmulf  21388  dv11cn  21442  plyaddlem1  21650  plyaddlem  21652  coeeulem  21661  coeaddlem  21685  coemulc  21691  dgradd2  21704  dgrcolem2  21710  ofmulrt  21717  plydivlem3  21730  plydivlem4  21731  plydiveu  21733  plyrem  21740  vieta1lem2  21746  elqaalem3  21756  qaa  21758  jensenlem2  22350  jensen  22351  basellem7  22393  basellem9  22395  dchrmulcl  22557  chssoc  24844  chjidm  24868  mdslmd3i  25681  inin  25841  disjnf  25861  ofrn  25902  ofrn2  25903  ofresid  25905  offval2f  25928  gsumle  26193  hauseqcn  26273  ofcof  26497  sibfof  26674  ofccat  26889  plymul02  26895  signshf  26937  nepss  27321  predidm  27596  itg2addnclem  28386  itg2addnclem3  28388  itg2addnc  28389  ftc1anclem3  28412  ftc1anclem5  28414  ftc1anclem6  28415  ftc1anclem8  28417  blbnd  28629  mzpclall  29006  mzpindd  29025  dgrsub2  29434  mpaaeu  29450  mendrng  29492  caofcan  29540  ofmul12  29542  ofdivrec  29543  ofdivcan4  29544  ofdivdiv2  29545  expgrowth  29552  ofaddmndmap  30676  mndpsuppss  30719  mndpfsupp  30724  matplusgcell  30761  matsubgcell  30762  mat1dimscm  30772  dflinc2  30803  bj-inrab2  32193  lshpinN  32385  lfladdcl  32467  lflvscl  32473  ldualvaddval  32527  lclkrlem2e  34907