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  13155  strressid  13156  ressinbasd  13159  grpressid  13646  gsumfzmptfidmadd  13928  lcomf  14344  crng2idl  14548  psrbaglesuppg  14689  psraddcl  14697  mplsubgfilemcl  14716  baspartn  14777  epttop  14817  dvaddxxbr  15428  dvmulxxbr  15429  dvaddxx  15430  dvmulxx  15431  dviaddf  15432  dvimulf  15433  plyaddlem1  15474  plyaddlem  15476