Theorem inidm 3416

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

Syntax hints:   = wceq 1397   ∈ wcel 2202   ∩ cin 3199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206

This theorem is referenced by:  inindi  3424  inindir  3425  uneqin  3458  ssdifeq0  3577  intsng  3962  xpindi  4865  xpindir  4866  resindm  5055  ofres  6250  offval2  6251  ofrfval2  6252  suppssof1  6253  ofco  6254  offveqb  6255  ofc1g  6257  ofc2g  6258  caofref  6260  caofrss  6267  caoftrn  6268  undifdc  7116  ofnegsub  9142  ressbasid  13171  strressid  13172  ressinbasd  13175  grpressid  13662  gsumfzmptfidmadd  13944  lcomf  14360  crng2idl  14564  psrbaglesuppg  14705  psraddcl  14713  mplsubgfilemcl  14732  baspartn  14793  epttop  14833  dvaddxxbr  15444  dvmulxxbr  15445  dvaddxx  15446  dvmulxx  15447  dviaddf  15448  dvimulf  15449  plyaddlem1  15490  plyaddlem  15492