Theorem inidm 3648

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

Syntax hints:   = wceq 1405   e. wcel 1842   i^i cin 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-in 3421

This theorem is referenced by:  inindi  3656  inindir  3657  uneqin  3701  ssdifeq0  3854  intsng  4263  xpindi  4957  xpindir  4958  resindm  5138  predidm  5389  offval2f  6533  fnfvof  6535  ofres  6537  offval2  6538  ofrfval2  6539  suppssof1OLD  6541  ofco  6542  offveq  6543  offveqb  6544  ofc1  6545  ofc2  6546  caofref  6548  caofrss  6555  caoftrn  6557  suppssof1  6936  suppofss1d  6940  suppofss2d  6941  fisn  7921  dffi3  7925  ofsubeq0  10573  ofnegsub  10574  ofsubge0  10575  seqof  12208  incexc  13800  sadeq  14331  smuval2  14341  smumul  14352  ressinbas  14904  pwsle  15106  pwsleval  15107  ghmplusg  17176  gsumzaddlem  17258  gsumzadd  17259  gsumzaddlemOLD  17260  gsumzaddOLD  17261  lcomf  17868  lcomfsupp  17870  crng2idl  18207  psrbaglesupp  18337  psrbaglesuppOLD  18338  psrbagaddcl  18340  psrbagaddclOLD  18341  psrbagcon  18342  psrbaglefi  18343  psrbaglefiOLD  18344  psrbagconf1o  18346  gsumbagdiaglem  18347  psraddcl  18356  psrvscacl  18366  psrlidm  18376  psrlidmOLD  18377  psrdi  18381  psrdir  18382  mplsubglem  18413  mplsubglemOLD  18415  psrbagev1  18497  psrbagev1OLD  18498  evlslem3  18503  evlslem1  18504  psrplusgpropd  18597  coe1add  18625  pf1ind  18711  frlmipval  19106  frlmphllem  19107  frlmphl  19108  frlmsslsp  19123  frlmup1  19125  mndvcl  19185  matplusgcell  19227  matsubgcell  19228  mat1dimscm  19269  baspartn  19747  indistopon  19794  epttop  19802  dissnlocfin  20322  ptbasin  20370  snfil  20657  tsmsadd  20941  ust0  21014  ustuqtop1  21036  rrxcph  22116  rrxds  22117  volun  22247  mbfmulc2lem  22346  mbfaddlem  22359  0pledm  22372  i1faddlem  22392  i1fmullem  22393  i1fadd  22394  i1fmul  22395  itg1addlem4  22398  i1fmulclem  22401  i1fmulc  22402  itg1lea  22411  itg1le  22412  mbfi1fseqlem5  22418  mbfi1flimlem  22421  mbfmullem2  22423  xrge0f  22430  itg2ge0  22434  itg2lea  22443  itg2mulclem  22445  itg2mulc  22446  itg2splitlem  22447  itg2split  22448  itg2monolem1  22449  itg2mono  22452  itg2i1fseqle  22453  itg2i1fseq  22454  itg2addlem  22457  itg2cnlem1  22460  dvaddf  22637  dvmulf  22638  dvcmulf  22640  dv11cn  22694  plyaddlem1  22902  plyaddlem  22904  coeeulem  22913  coeaddlem  22938  coemulc  22944  dgradd2  22957  dgrcolem2  22963  ofmulrt  22970  plydivlem3  22983  plydivlem4  22984  plydiveu  22986  plyrem  22993  vieta1lem2  22999  elqaalem3  23009  qaa  23011  jensenlem2  23643  jensen  23644  basellem7  23741  basellem9  23743  dchrmulcl  23905  chssoc  26828  chjidm  26852  mdslmd3i  27664  inin  27828  disjnf  27863  ofrn  27922  ofrn2  27923  ofresid  27925  gsumle  28221  hauseqcn  28330  ofcof  28554  carsgclctunlem1  28765  carsgclctun  28769  sibfof  28788  ofccat  29003  plymul02  29009  signshf  29051  msrid  29757  nepss  29924  bj-inrab2  31060  itg2addnclem  31439  itg2addnclem3  31441  itg2addnc  31442  ftc1anclem3  31465  ftc1anclem5  31467  ftc1anclem6  31468  ftc1anclem8  31470  blbnd  31565  lshpinN  32007  lfladdcl  32089  lflvscl  32095  ldualvaddval  32149  lclkrlem2e  34531  mzpclall  35021  mzpindd  35040  dgrsub2  35448  mpaaeu  35463  mendring  35505  corclrcl  35686  relexpaddss  35697  caofcan  36076  ofmul12  36078  ofdivrec  36079  ofdivcan4  36080  ofdivdiv2  36081  expgrowth  36088  binomcxplemrat  36103  binomcxplemnotnn0  36109  dvsinax  37076  dvcosax  37091  dvdivcncf  37092  uzlidlring  38246  ofaddmndmap  38444  mndpsuppss  38475  mndpfsupp  38480  dmatALTbas  38513  dflinc2  38522  fdivmpt  38671  aacllem  38860