Theorem inidm 3562

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 3547	1 |- ( A i^i A ) = A

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

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 2423

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 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338

This theorem is referenced by:  inindi  3570  inindir  3571  uneqin  3604  ssdifeq0  3764  intsng  4166  xpindi  4976  xpindir  4977  resindm  5154  fnfvof  6336  ofres  6338  offval2  6339  ofrfval2  6340  suppssof1OLD  6342  ofco  6343  offveq  6344  offveqb  6345  ofc1  6346  ofc2  6347  caofref  6349  caofrss  6356  caoftrn  6358  suppssof1  6725  suppofss1d  6729  suppofss2d  6730  fisn  7680  dffi3  7684  ofsubeq0  10322  ofnegsub  10323  ofsubge0  10324  seqof  11866  incexc  13303  sadeq  13671  smuval2  13681  smumul  13692  ressinbas  14237  pwsle  14433  pwsleval  14434  ghmplusg  16331  gsumzaddlem  16411  gsumzadd  16412  gsumzaddlemOLD  16413  gsumzaddOLD  16414  lcomf  16986  lcomfsupp  16988  crng2idl  17324  psrbaglesupp  17438  psrbaglesuppOLD  17439  psrbagaddcl  17441  psrbagaddclOLD  17442  psrbagcon  17443  psrbaglefi  17444  psrbaglefiOLD  17445  psrbagconf1o  17447  gsumbagdiaglem  17448  psraddcl  17457  psrvscacl  17467  psrlidm  17477  psrlidmOLD  17478  psrdi  17482  psrdir  17483  mplsubglem  17513  mplsubglemOLD  17515  psrbagev1  17597  psrbagev1OLD  17598  evlslem3  17603  evlslem1  17604  psrplusgpropd  17693  coe1add  17721  pf1ind  17792  frlmipval  18207  frlmphllem  18208  frlmphl  18209  frlmsslsp  18226  frlmsslspOLD  18227  frlmup1  18229  mndvcl  18294  baspartn  18562  indistopon  18608  epttop  18616  ptbasin  19153  snfil  19440  tsmsadd  19724  ust0  19797  ustuqtop1  19819  rrxcph  20899  rrxds  20900  volun  21029  mbfmulc2lem  21128  mbfaddlem  21141  0pledm  21154  i1faddlem  21174  i1fmullem  21175  i1fadd  21176  i1fmul  21177  itg1addlem4  21180  i1fmulclem  21183  i1fmulc  21184  itg1lea  21193  itg1le  21194  mbfi1fseqlem5  21200  mbfi1flimlem  21203  mbfmullem2  21205  xrge0f  21212  itg2ge0  21216  itg2lea  21225  itg2mulclem  21227  itg2mulc  21228  itg2splitlem  21229  itg2split  21230  itg2monolem1  21231  itg2mono  21234  itg2i1fseqle  21235  itg2i1fseq  21236  itg2addlem  21239  itg2cnlem1  21242  dvaddf  21419  dvmulf  21420  dvcmulf  21422  dv11cn  21476  plyaddlem1  21684  plyaddlem  21686  coeeulem  21695  coeaddlem  21719  coemulc  21725  dgradd2  21738  dgrcolem2  21744  ofmulrt  21751  plydivlem3  21764  plydivlem4  21765  plydiveu  21767  plyrem  21774  vieta1lem2  21780  elqaalem3  21790  qaa  21792  jensenlem2  22384  jensen  22385  basellem7  22427  basellem9  22429  dchrmulcl  22591  chssoc  24902  chjidm  24926  mdslmd3i  25739  inin  25899  disjnf  25919  ofrn  25960  ofrn2  25961  ofresid  25963  offval2f  25986  gsumle  26249  hauseqcn  26328  ofcof  26552  sibfof  26729  ofccat  26944  plymul02  26950  signshf  26992  nepss  27377  predidm  27652  itg2addnclem  28446  itg2addnclem3  28448  itg2addnc  28449  ftc1anclem3  28472  ftc1anclem5  28474  ftc1anclem6  28475  ftc1anclem8  28477  blbnd  28689  mzpclall  29066  mzpindd  29085  dgrsub2  29494  mpaaeu  29510  mendrng  29552  caofcan  29600  ofmul12  29602  ofdivrec  29603  ofdivcan4  29604  ofdivdiv2  29605  expgrowth  29612  ofaddmndmap  30737  mndpsuppss  30787  mndpfsupp  30793  matplusgcell  30862  matsubgcell  30863  mat1dimscm  30874  dflinc2  30947  bj-inrab2  32434  lshpinN  32637  lfladdcl  32719  lflvscl  32725  ldualvaddval  32779  lclkrlem2e  35159