---

Step * of Lemma fset-member-add-name

∀I:fset(ℕ). ∀i,j:ℕ.  uiff(j ∈ I+i;(j = i ∈ ℤ) ∨ j ∈ I)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `add-name` 0
   THEN Unfold `names-deq` 0
   THEN RWO "member-fset-add" 0
   THEN Auto
   THEN Unhide
   THEN Auto
   THEN RepeatFor 2 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{}).  \mforall{}i,j:\mBbbN{}.    uiff(j  \mmember{}  I+i;(j  =  i)  \mvee{}  j  \mmember{}  I)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `add-name`  0
  THEN  Unfold  `names-deq`  0
  THEN  RWO  "member-fset-add"  0
  THEN  Auto
  THEN  Unhide
  THEN  Auto
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index