---

Step * of Lemma member-nameset-diff

∀[L,X:Cname List]. ∀[x:nameset(L)].  x ∈ nameset(L-X) supposing ¬(x ∈ X)
BY
{ Auto }

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

---

Latex:

---

Latex:
\mforall{}[L,X:Cname  List].  \mforall{}[x:nameset(L)].    x  \mmember{}  nameset(L-X)  supposing  \mneg{}(x  \mmember{}  X)


By

---

Latex:
Auto

---

Home Index