Theorem inidm 3429

Description: Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
inidm	|- ( A i^i A ) = A

Proof of Theorem inidm

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		anidm 396	. 2 |- ( ( x e. A /\ x e. A ) <-> x e. A )
2	1	ineqri 3413	1 |- ( A i^i A ) = A

Syntax hints:   = wceq 1398   e. wcel 2203   i^i cin 3209

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-in 3216

This theorem is referenced by:  inindi  3437  inindir  3438  uneqin  3471  ssdifeq0  3591  intsng  3982  xpindi  4889  xpindir  4890  resindm  5079  ofres  6280  offval2  6281  ofrfval2  6282  suppssof1  6283  ofco  6284  offveqb  6285  ofc1g  6287  ofc2g  6288  caofref  6290  caofrss  6297  caoftrn  6298  suppofss1dcl  6463  suppofss2dcl  6464  undifdc  7183  ofnegsub  9235  ressbasid  13275  strressid  13276  ressinbasd  13279  grpressid  13766  gsumfzmptfidmadd  14048  lcomf  14467  crng2idl  14671  psrbaglesuppg  14813  psrbagaddclfi  14817  psrbagcon  14818  psrbagconf1o  14820  psraddcl  14827  mplsubgfilemcl  14846  baspartn  14907  epttop  14947  dvaddxxbr  15558  dvmulxxbr  15559  dvaddxx  15560  dvmulxx  15561  dviaddf  15562  dvimulf  15563  plyaddlem1  15604  plyaddlem  15606