Theorem inidm 4126

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 575	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	ineqri 4112	1 ⊢ (𝐴 ∩ 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  inindi  4134  inindir  4135  uneqin  4237  disjeq0  4412  ssdifeq0  4445  intsng  4946  xpindi  5815  xpindir  5816  resindmOLD  6026  elidinxpid  6043  idinxpresid  6046  predidm  6336  offval2f  7718  fnfvof  7720  ofres  7722  offval2  7723  ofrfval2  7724  coof  7727  ofco  7728  offveq  7729  offveqb  7730  ofc1  7731  ofc2  7732  caofref  7734  caofrss  7742  caoftrn  7744  offsplitfpar  8143  suppssof1  8230  suppofssd  8234  suppofss1d  8235  suppofss2d  8236  fisn  9432  dffi3  9436  ofsubeq0  12330  ofnegsub  12331  ofsubge0  12332  seqof  14215  ofccat  15137  incexc  16021  sadeq  16657  smuval2  16667  smumul  16678  ressinbas  17438  pwsle  17679  pwsleval  17680  mndpsuppss  18974  mndvcl  19007  ghmplusg  20075  gsumzaddlem  20150  gsumzadd  20151  gsumle  20374  pwspjmhmmgpd  20572  lcomf  21191  crng2idl  21591  frlmipval  22100  frlmphllem  22101  frlmphl  22102  frlmsslsp  22117  frlmup1  22119  psrbaglesupp  22245  psrbagaddcl  22247  psrbagcon  22248  psrbaglefi  22249  psrbagleadd1  22251  psrbagconf1o  22252  gsumbagdiaglem  22254  psraddcl  22262  psrvscacl  22274  psrlidm  22284  psrdi  22287  psrdir  22288  psrascl  22301  mplsubglem  22321  psrbagev1  22401  evlslem3  22404  evlslem1  22406  evlsvvval  22417  mplmapghm  22446  mhpmulcl  22485  psdmplcl  22498  psdadd  22499  psdmul  22502  psdmvr  22505  psrplusgpropd  22568  coe1add  22598  pf1ind  22688  evls1fpws  22702  matplusgcell  22763  matsubgcell  22764  mat1dimscm  22805  matunitlindflem1  23009  matunitlindflem2  23010  baspartn  23287  indistopon  23334  epttop  23342  dissnlocfin  23863  ptbasin  23911  snfil  24198  tsmsadd  24481  ust0  24554  ustuqtop1  24575  rrxcph  25728  rrxds  25729  volun  25881  mbfmulc2lem  25983  mbfaddlem  25996  0pledm  26009  i1faddlem  26029  i1fmullem  26030  i1fadd  26031  i1fmul  26032  itg1addlem4  26035  i1fmulclem  26038  i1fmulc  26039  itg1lea  26048  itg1le  26049  mbfi1fseqlem5  26055  mbfi1flimlem  26058  mbfmullem2  26060  xrge0f  26067  itg2ge0  26071  itg2lea  26080  itg2mulclem  26082  itg2mulc  26083  itg2splitlem  26084  itg2split  26085  itg2monolem1  26086  itg2mono  26089  itg2i1fseqle  26090  itg2i1fseq  26091  itg2addlem  26094  itg2cnlem1  26097  dvaddf  26277  dvmulf  26278  dvcmulf  26280  dv11cn  26336  plyaddlem1  26547  plyaddlem  26549  coeeulem  26558  coeaddlem  26583  coemulc  26589  dgradd2  26602  dgrcolem2  26608  ofmulrt  26615  plymul02  26616  plydivlem3  26631  plydivlem4  26632  plydiveu  26634  plyrem  26641  rnplynfin  26645  vieta1lem2  26649  elqaalem3  26659  qaa  26662  jensenlem2  27330  jensen  27331  basellem7  27429  basellem9  27431  dchrmulcl  27591  chssoc  32113  chjidm  32137  mdslmd3i  32949  inin  33169  unidifsnne  33189  disjnf  33221  fnfvor  33260  ofrco  33261  ofrn  33290  ofrn2  33291  ofresid  33293  offinsupp1  33374  tocyccntz  33761  elrgspnlem1  33859  islinds5  33979  ellspds  33980  1arithidomlem2  34124  1arithidom  34125  ply1gsumz  34187  0mplrim  34202  selvply1rhmlemb  34207  selvply1rhmlem4  34211  mplvrpmrhm  34235  esplyind  34263  ply1degltdimlem  34310  fedgmullem1  34317  extdgfialglem2  34381  hauseqcn  34586  ofcof  34795  carsgclctunlem1  35005  carsgclctun  35009  sibfof  35028  signshf  35273  circlemethhgt  35328  msrid  36434  nepss  36616  bj-inrab2  37974  poimirlem1  38685  poimirlem2  38686  poimirlem4  38688  poimirlem6  38690  poimirlem7  38691  poimirlem8  38692  poimirlem10  38694  poimirlem11  38695  poimirlem12  38696  poimirlem16  38700  poimirlem17  38701  poimirlem19  38703  poimirlem20  38704  poimirlem23  38707  poimirlem24  38708  poimirlem25  38709  poimirlem28  38712  poimirlem29  38713  poimirlem30  38714  poimirlem31  38715  poimirlem32  38716  broucube  38718  itg2addnclem  38735  itg2addnclem3  38737  itg2addnc  38738  ftc1anclem3  38759  ftc1anclem5  38761  ftc1anclem6  38762  ftc1anclem8  38764  blbnd  38867  disjimeceqim  39882  lshpinN  40192  lfladdcl  40274  lflvscl  40280  ldualvaddval  40334  lclkrlem2e  42714  ofun  43435  fsuppind  43764  fsuppssind  43767  mhphf  43771  mzpclall  43884  mzpindd  43903  dgrsub2  44283  mpaaeu  44298  mendring  44336  ofoafo  44504  ofoacl  44505  ofoaid1  44506  ofoaid2  44507  ofoaass  44508  ofoacom  44509  naddcnff  44510  naddcnffo  44512  naddcnfcom  44514  naddcnfid1  44515  naddcnfass  44517  relexpaddss  44864  ntrkbimka  45184  clsk3nimkb  45186  caofcan  45453  ofmul12  45455  ofdivrec  45456  ofdivcan4  45457  ofdivdiv2  45458  expgrowth  45465  binomcxplemrat  45480  binomcxplemnotnn0  45486  disjf1  46343  dvsinax  47068  dvcosax  47081  dvdivcncf  47082  meadjun  47617  smfmulc1  47951  cjnpoly  48084  f1cof1blem  48289  isubgr0uhgr  49116  uzlidlring  49477  ofaddmndmap  49600  dmatALTbas  49658  dflinc2  49667  fdivmpt  49797  zeroopropdlem  50509  incat  50884  aacllem  51159  veroquadmodzerod  51204  amgmwlem  51207