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  6249  offval2  6250  ofrfval2  6251  suppssof1  6252  ofco  6253  offveqb  6254  ofc1g  6256  ofc2g  6257  caofref  6259  caofrss  6266  caoftrn  6267  undifdc  7115  ofnegsub  9141  ressbasid  13152  strressid  13153  ressinbasd  13156  grpressid  13643  gsumfzmptfidmadd  13925  lcomf  14340  crng2idl  14544  psrbaglesuppg  14685  psraddcl  14693  mplsubgfilemcl  14712  baspartn  14773  epttop  14813  dvaddxxbr  15424  dvmulxxbr  15425  dvaddxx  15426  dvmulxx  15427  dviaddf  15428  dvimulf  15429  plyaddlem1  15470  plyaddlem  15472