Theorem inidm 4156

Description: Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
inidm	⊢ (𝐴 ∩ 𝐴) = 𝐴

Proof of Theorem inidm

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		anidm 569	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	ineqri 4142	1 ⊢ (𝐴 ∩ 𝐴) = 𝐴

Syntax hints:   = wceq 1547   ∈ wcel 2119   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  inindi  4164  inindir  4165  uneqin  4218  disjeq0  4385  ssdifeq0  4415  intsng  4914  xpindi  5776  xpindir  5777  resindm  5983  elidinxpid  5998  idinxpresid  6001  predidm  6278  offval2f  7636  fnfvof  7638  ofres  7640  offval2  7641  ofrfval2  7642  coof  7645  ofco  7646  offveq  7647  offveqb  7648  ofc1  7649  ofc2  7650  caofref  7652  caofrss  7660  caoftrn  7662  offsplitfpar  8059  suppssof1  8140  suppofssd  8144  suppofss1d  8145  suppofss2d  8146  fisn  9331  dffi3  9335  ofsubeq0  12148  ofnegsub  12149  ofsubge0  12150  seqof  14013  ofccat  14923  incexc  15794  sadeq  16433  smuval2  16443  smumul  16454  ressinbas  17207  pwsle  17448  pwsleval  17449  mndpsuppss  18725  mndvcl  18757  ghmplusg  19813  gsumzaddlem  19888  gsumzadd  19889  gsumle  20112  pwspjmhmmgpd  20299  lcomf  20892  crng2idl  21275  frlmipval  21755  frlmphllem  21756  frlmphl  21757  frlmsslsp  21772  frlmup1  21774  psrbaglesupp  21898  psrbagaddcl  21900  psrbagcon  21901  psrbaglefi  21902  psrbagleadd1  21904  psrbagconf1o  21905  gsumbagdiaglem  21907  psraddcl  21915  psrvscacl  21927  psrlidm  21937  psrdi  21940  psrdir  21941  psrascl  21954  mplsubglem  21974  psrbagev1  22054  evlslem3  22057  evlslem1  22059  evlsvvval  22070  mplmapghm  22099  mhpmulcl  22138  psdmplcl  22151  psdadd  22152  psdmul  22155  psdmvr  22158  psrplusgpropd  22221  coe1add  22251  pf1ind  22342  evls1fpws  22356  matplusgcell  22417  matsubgcell  22418  mat1dimscm  22459  baspartn  22938  indistopon  22985  epttop  22993  dissnlocfin  23513  ptbasin  23561  snfil  23848  tsmsadd  24131  ust0  24204  ustuqtop1  24225  rrxcph  25378  rrxds  25379  volun  25531  mbfmulc2lem  25633  mbfaddlem  25646  0pledm  25659  i1faddlem  25679  i1fmullem  25680  i1fadd  25681  i1fmul  25682  itg1addlem4  25685  i1fmulclem  25688  i1fmulc  25689  itg1lea  25698  itg1le  25699  mbfi1fseqlem5  25705  mbfi1flimlem  25708  mbfmullem2  25710  xrge0f  25717  itg2ge0  25721  itg2lea  25730  itg2mulclem  25732  itg2mulc  25733  itg2splitlem  25734  itg2split  25735  itg2monolem1  25736  itg2mono  25739  itg2i1fseqle  25740  itg2i1fseq  25741  itg2addlem  25744  itg2cnlem1  25747  dvaddf  25928  dvmulf  25929  dvcmulf  25931  dv11cn  25987  plyaddlem1  26197  plyaddlem  26199  coeeulem  26208  coeaddlem  26233  coemulc  26239  dgradd2  26252  dgrcolem2  26258  ofmulrt  26267  plydivlem3  26280  plydivlem4  26281  plydiveu  26283  plyrem  26290  vieta1lem2  26296  elqaalem3  26306  qaa  26308  jensenlem2  26970  jensen  26971  basellem7  27069  basellem9  27071  dchrmulcl  27231  chssoc  31586  chjidm  31610  mdslmd3i  32422  inin  32605  unidifsnne  32625  disjnf  32660  fnfvor  32702  ofrco  32703  ofrn  32732  ofrn2  32733  ofresid  32735  offinsupp1  32819  tocyccntz  33226  elrgspnlem1  33324  islinds5  33451  ellspds  33452  1arithidomlem2  33628  1arithidom  33629  ply1gsumz  33691  0mplrim  33707  selvply1rhmlemb  33712  selvply1rhmlem4  33716  mplvrpmrhm  33740  esplyind  33768  ply1degltdimlem  33815  fedgmullem1  33822  extdgfialglem2  33886  hauseqcn  34091  ofcof  34300  carsgclctunlem1  34510  carsgclctun  34514  sibfof  34533  plymul02  34739  signshf  34781  circlemethhgt  34836  msrid  35782  nepss  35955  bj-inrab2  37290  matunitlindflem1  37992  matunitlindflem2  37993  poimirlem1  37997  poimirlem2  37998  poimirlem3  37999  poimirlem4  38000  poimirlem6  38002  poimirlem7  38003  poimirlem8  38004  poimirlem10  38006  poimirlem11  38007  poimirlem12  38008  poimirlem16  38012  poimirlem17  38013  poimirlem19  38015  poimirlem20  38016  poimirlem23  38019  poimirlem24  38020  poimirlem25  38021  poimirlem28  38024  poimirlem29  38025  poimirlem30  38026  poimirlem31  38027  poimirlem32  38028  broucube  38030  itg2addnclem  38047  itg2addnclem3  38049  itg2addnc  38050  ftc1anclem3  38071  ftc1anclem5  38073  ftc1anclem6  38074  ftc1anclem8  38076  blbnd  38163  disjimeceqim  39180  lshpinN  39490  lfladdcl  39572  lflvscl  39578  ldualvaddval  39632  lclkrlem2e  42012  ofun  42731  fsuppind  43049  fsuppssind  43052  mhphf  43056  mzpclall  43185  mzpindd  43204  dgrsub2  43589  mpaaeu  43604  mendring  43642  ofoafo  43810  ofoacl  43811  ofoaid1  43812  ofoaid2  43813  ofoaass  43814  ofoacom  43815  naddcnff  43816  naddcnffo  43818  naddcnfcom  43820  naddcnfid1  43821  naddcnfass  43823  relexpaddss  44171  ntrkbimka  44491  clsk3nimkb  44493  caofcan  44776  ofmul12  44778  ofdivrec  44779  ofdivcan4  44780  ofdivdiv2  44781  expgrowth  44788  binomcxplemrat  44803  binomcxplemnotnn0  44809  disjf1  45638  dvsinax  46364  dvcosax  46377  dvdivcncf  46378  meadjun  46913  smfmulc1  47247  cjnpoly  47360  f1cof1blem  47545  isubgr0uhgr  48372  uzlidlring  48734  ofaddmndmap  48842  dmatALTbas  48900  dflinc2  48909  fdivmpt  49039  zeroopropdlem  49740  incat  50099  aacllem  50299  amgmwlem  50300