Theorem inidm 3414

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

Syntax hints:   = wceq 1395   ∈ wcel 2200   ∩ cin 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-in 3204

This theorem is referenced by:  inindi  3422  inindir  3423  uneqin  3456  ssdifeq0  3575  intsng  3960  xpindi  4863  xpindir  4864  resindm  5053  ofres  6245  offval2  6246  ofrfval2  6247  suppssof1  6248  ofco  6249  offveqb  6250  ofc1g  6252  ofc2g  6253  caofref  6255  caofrss  6262  caoftrn  6263  undifdc  7109  ofnegsub  9132  ressbasid  13143  strressid  13144  ressinbasd  13147  grpressid  13634  gsumfzmptfidmadd  13916  lcomf  14331  crng2idl  14535  psrbaglesuppg  14676  psraddcl  14684  mplsubgfilemcl  14703  baspartn  14764  epttop  14804  dvaddxxbr  15415  dvmulxxbr  15416  dvaddxx  15417  dvmulxx  15418  dviaddf  15419  dvimulf  15420  plyaddlem1  15461  plyaddlem  15463