Theorem inidm 3413

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

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

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 2801  df-in 3203

This theorem is referenced by:  inindi  3421  inindir  3422  uneqin  3455  ssdifeq0  3574  intsng  3957  xpindi  4857  xpindir  4858  resindm  5047  ofres  6239  offval2  6240  ofrfval2  6241  suppssof1  6242  ofco  6243  offveqb  6244  ofc1g  6246  ofc2g  6247  caofref  6249  caofrss  6256  caoftrn  6257  undifdc  7097  ofnegsub  9120  ressbasid  13119  strressid  13120  ressinbasd  13123  grpressid  13610  gsumfzmptfidmadd  13892  lcomf  14307  crng2idl  14511  psrbaglesuppg  14652  psraddcl  14660  mplsubgfilemcl  14679  baspartn  14740  epttop  14780  dvaddxxbr  15391  dvmulxxbr  15392  dvaddxx  15393  dvmulxx  15394  dviaddf  15395  dvimulf  15396  plyaddlem1  15437  plyaddlem  15439