Theorem inidm 3784

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

Syntax hints:   = wceq 1475   ∈ wcel 1977   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  inindi  3792  inindir  3793  uneqin  3837  ssdifeq0  4003  intsng  4447  xpindi  5177  xpindir  5178  resindm  5364  predidm  5619  offval2f  6807  fnfvof  6809  ofres  6811  offval2  6812  ofrfval2  6813  ofco  6815  offveq  6816  offveqb  6817  ofc1  6818  ofc2  6819  caofref  6821  caofrss  6828  caoftrn  6830  suppssof1  7215  suppofss1d  7219  suppofss2d  7220  fisn  8216  dffi3  8220  ofsubeq0  10894  ofnegsub  10895  ofsubge0  10896  seqof  12720  ofccat  13556  incexc  14408  sadeq  15032  smuval2  15042  smumul  15053  ressinbas  15763  pwsle  15975  pwsleval  15976  ghmplusg  18072  gsumzaddlem  18144  gsumzadd  18145  lcomf  18725  lcomfsupp  18726  crng2idl  19060  psrbaglesupp  19189  psrbagaddcl  19191  psrbagcon  19192  psrbaglefi  19193  psrbagconf1o  19195  gsumbagdiaglem  19196  psraddcl  19204  psrvscacl  19214  psrlidm  19224  psrdi  19227  psrdir  19228  mplsubglem  19255  psrbagev1  19331  evlslem3  19335  evlslem1  19336  psrplusgpropd  19427  coe1add  19455  pf1ind  19540  frlmipval  19937  frlmphllem  19938  frlmphl  19939  frlmsslsp  19954  frlmup1  19956  mndvcl  20016  matplusgcell  20058  matsubgcell  20059  mat1dimscm  20100  baspartn  20569  indistopon  20615  epttop  20623  dissnlocfin  21142  ptbasin  21190  snfil  21478  tsmsadd  21760  ust0  21833  ustuqtop1  21855  rrxcph  22988  rrxds  22989  volun  23120  mbfmulc2lem  23220  mbfaddlem  23233  0pledm  23246  i1faddlem  23266  i1fmullem  23267  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  i1fmulclem  23275  i1fmulc  23276  itg1lea  23285  itg1le  23286  mbfi1fseqlem5  23292  mbfi1flimlem  23295  mbfmullem2  23297  xrge0f  23304  itg2ge0  23308  itg2lea  23317  itg2mulclem  23319  itg2mulc  23320  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq  23328  itg2addlem  23331  itg2cnlem1  23334  dvaddf  23511  dvmulf  23512  dvcmulf  23514  dv11cn  23568  plyaddlem1  23773  plyaddlem  23775  coeeulem  23784  coeaddlem  23809  coemulc  23815  dgradd2  23828  dgrcolem2  23834  ofmulrt  23841  plydivlem3  23854  plydivlem4  23855  plydiveu  23857  plyrem  23864  vieta1lem2  23870  elqaalem3  23880  qaa  23882  jensenlem2  24514  jensen  24515  basellem7  24613  basellem9  24615  dchrmulcl  24774  chssoc  27739  chjidm  27763  mdslmd3i  28575  inin  28737  disjnf  28766  ofrn  28821  ofrn2  28822  ofresid  28824  gsumle  29110  hauseqcn  29269  ofcof  29496  carsgclctunlem1  29706  carsgclctun  29710  sibfof  29729  plymul02  29949  signshf  29991  msrid  30696  nepss  30854  bj-inrab2  32116  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  broucube  32613  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  ftc1anclem3  32657  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem8  32662  blbnd  32756  lshpinN  33294  lfladdcl  33376  lflvscl  33382  ldualvaddval  33436  lclkrlem2e  35818  mzpclall  36308  mzpindd  36327  dgrsub2  36724  mpaaeu  36739  mendring  36781  corclrcl  37018  relexpaddss  37029  ntrkbimka  37356  clsk3nimkb  37358  caofcan  37544  ofmul12  37546  ofdivrec  37547  ofdivcan4  37548  ofdivdiv2  37549  expgrowth  37556  binomcxplemrat  37571  binomcxplemnotnn0  37577  disjf1  38364  dvsinax  38801  dvcosax  38816  dvdivcncf  38817  meadjun  39355  smfmulc1  39681  uzlidlring  41719  ofaddmndmap  41915  mndpsuppss  41946  mndpfsupp  41951  dmatALTbas  41984  dflinc2  41993  fdivmpt  42132  aacllem  42356  amgmwlem  42357