ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  inidm GIF version

Theorem inidm 3289
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.
StepHypRef Expression
1 anidm 394 . 2 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
21ineqri 3273 1 (𝐴𝐴) = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1332  wcel 1481  cin 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3081
This theorem is referenced by:  inindi  3297  inindir  3298  uneqin  3331  ssdifeq0  3449  intsng  3812  xpindi  4681  xpindir  4682  resindm  4868  ofres  6003  offval2  6004  ofrfval2  6005  suppssof1  6006  ofco  6007  offveqb  6008  caofref  6010  caofrss  6013  caoftrn  6014  undifdc  6819  baspartn  12254  epttop  12296  dvaddxxbr  12871  dvmulxxbr  12872  dvaddxx  12873  dvmulxx  12874  dviaddf  12875  dvimulf  12876
  Copyright terms: Public domain W3C validator