---

Step * 1 of Lemma mset_mem_diff


1. s : DSet
2. as : DisList{s}
3. bs : |s| List
4. c : |s|
⊢ c ∈b (as - bs) = (c ∈b as) ∧b (¬b(c ∈b bs))
BY
{ ((BLemma `mem_diff`) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  DisList\{s\}
3.  bs  :  |s|  List
4.  c  :  |s|
\mvdash{}  c  \mmember{}\msubb{}  (as  -  bs)  =  (c  \mmember{}\msubb{}  as)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(c  \mmember{}\msubb{}  bs))


By

---

Latex:
((BLemma  `mem\_diff`)  THEN  Auto)

---

Home Index