Theorem inidm 3372

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 3356	1 ⊢ (𝐴 ∩ 𝐴) = 𝐴

Syntax hints:   = wceq 1364   ∈ wcel 2167   ∩ cin 3156

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163

This theorem is referenced by:  inindi  3380  inindir  3381  uneqin  3414  ssdifeq0  3533  intsng  3908  xpindi  4801  xpindir  4802  resindm  4988  ofres  6150  offval2  6151  ofrfval2  6152  suppssof1  6153  ofco  6154  offveqb  6155  ofc1g  6156  ofc2g  6157  caofref  6159  caofrss  6162  caoftrn  6163  undifdc  6985  ofnegsub  8989  ressbasid  12748  strressid  12749  ressinbasd  12752  grpressid  13193  gsumfzmptfidmadd  13469  lcomf  13883  crng2idl  14087  psrbaglesuppg  14226  psraddcl  14232  baspartn  14286  epttop  14326  dvaddxxbr  14937  dvmulxxbr  14938  dvaddxx  14939  dvmulxx  14940  dviaddf  14941  dvimulf  14942  plyaddlem1  14983  plyaddlem  14985