---

Step * 1 of Lemma member-nameset-diff


1. L : Cname List
2. X : Cname List
3. x : nameset(L)
4. ¬(x ∈ X)
⊢ x ∈ nameset(L-X)
BY
{ (DVar `x'⋅ THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. L : Cname List
2. X : Cname List
3. x : Cname
4. (x ∈ L)
5. ¬(x ∈ X)
⊢ (x ∈ L-X)

---

Latex:

---

Latex:

1.  L  :  Cname  List
2.  X  :  Cname  List
3.  x  :  nameset(L)
4.  \mneg{}(x  \mmember{}  X)
\mvdash{}  x  \mmember{}  nameset(L-X)


By

---

Latex:
(DVar  `x'\mcdot{}  THEN  MemTypeCD  THEN  Auto)

---

Home Index