Theorem inidm 3700

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

Syntax hints:   = wceq 1374   e. wcel 1762   i^i cin 3468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476

This theorem is referenced by:  inindi  3708  inindir  3709  uneqin  3742  ssdifeq0  3902  intsng  4310  xpindi  5127  xpindir  5128  resindm  5309  fnfvof  6528  ofres  6530  offval2  6531  ofrfval2  6532  suppssof1OLD  6534  ofco  6535  offveq  6536  offveqb  6537  ofc1  6538  ofc2  6539  caofref  6541  caofrss  6548  caoftrn  6550  suppssof1  6923  suppofss1d  6927  suppofss2d  6928  fisn  7876  dffi3  7880  ofsubeq0  10522  ofnegsub  10523  ofsubge0  10524  seqof  12120  incexc  13601  sadeq  13970  smuval2  13980  smumul  13991  ressinbas  14540  pwsle  14736  pwsleval  14737  ghmplusg  16638  gsumzaddlem  16718  gsumzadd  16719  gsumzaddlemOLD  16720  gsumzaddOLD  16721  lcomf  17324  lcomfsupp  17326  crng2idl  17662  psrbaglesupp  17781  psrbaglesuppOLD  17782  psrbagaddcl  17784  psrbagaddclOLD  17785  psrbagcon  17786  psrbaglefi  17787  psrbaglefiOLD  17788  psrbagconf1o  17790  gsumbagdiaglem  17791  psraddcl  17800  psrvscacl  17810  psrlidm  17820  psrlidmOLD  17821  psrdi  17825  psrdir  17826  mplsubglem  17857  mplsubglemOLD  17859  psrbagev1  17941  psrbagev1OLD  17942  evlslem3  17947  evlslem1  17948  psrplusgpropd  18041  coe1add  18069  pf1ind  18155  frlmipval  18570  frlmphllem  18571  frlmphl  18572  frlmsslsp  18589  frlmsslspOLD  18590  frlmup1  18592  mndvcl  18653  matplusgcell  18695  matsubgcell  18696  mat1dimscm  18737  baspartn  19215  indistopon  19261  epttop  19269  ptbasin  19806  snfil  20093  tsmsadd  20377  ust0  20450  ustuqtop1  20472  rrxcph  21552  rrxds  21553  volun  21683  mbfmulc2lem  21782  mbfaddlem  21795  0pledm  21808  i1faddlem  21828  i1fmullem  21829  i1fadd  21830  i1fmul  21831  itg1addlem4  21834  i1fmulclem  21837  i1fmulc  21838  itg1lea  21847  itg1le  21848  mbfi1fseqlem5  21854  mbfi1flimlem  21857  mbfmullem2  21859  xrge0f  21866  itg2ge0  21870  itg2lea  21879  itg2mulclem  21881  itg2mulc  21882  itg2splitlem  21883  itg2split  21884  itg2monolem1  21885  itg2mono  21888  itg2i1fseqle  21889  itg2i1fseq  21890  itg2addlem  21893  itg2cnlem1  21896  dvaddf  22073  dvmulf  22074  dvcmulf  22076  dv11cn  22130  plyaddlem1  22338  plyaddlem  22340  coeeulem  22349  coeaddlem  22373  coemulc  22379  dgradd2  22392  dgrcolem2  22398  ofmulrt  22405  plydivlem3  22418  plydivlem4  22419  plydiveu  22421  plyrem  22428  vieta1lem2  22434  elqaalem3  22444  qaa  22446  jensenlem2  23038  jensen  23039  basellem7  23081  basellem9  23083  dchrmulcl  23245  chssoc  26076  chjidm  26100  mdslmd3i  26913  inin  27073  disjnf  27092  ofrn  27138  ofrn2  27139  ofresid  27141  offval2f  27164  gsumle  27419  hauseqcn  27499  ofcof  27732  sibfof  27908  ofccat  28123  plymul02  28129  signshf  28171  nepss  28556  predidm  28831  itg2addnclem  29630  itg2addnclem3  29632  itg2addnc  29633  ftc1anclem3  29656  ftc1anclem5  29658  ftc1anclem6  29659  ftc1anclem8  29661  blbnd  29873  mzpclall  30250  mzpindd  30269  dgrsub2  30677  mpaaeu  30693  mendrng  30735  caofcan  30783  ofmul12  30785  ofdivrec  30786  ofdivcan4  30787  ofdivdiv2  30788  expgrowth  30795  icccncfext  31181  dvsinax  31196  dvcosax  31211  dvdivcncf  31212  ofaddmndmap  31872  mndpsuppss  31912  mndpfsupp  31917  dmatALTbas  31950  dflinc2  31959  bj-inrab2  33452  lshpinN  33661  lfladdcl  33743  lflvscl  33749  ldualvaddval  33803  lclkrlem2e  36183