---

Step * of Lemma mem_diff

∀s:DSet. ∀as:DisList{s}. ∀bs:|s| List. ∀c:|s|.  c ∈b (as - bs) = (c ∈b as) ∧b (¬b(c ∈b bs))
BY
{ ((((RepD THENM BLemma `iff_imp_equal_bool`) THENM RW bool_to_propC 0) THENM RWH (LemmaC `mem_iff_count_nzero`) 0)
   THENA Auto
   ) }

1
1. s : DSet
2. as : DisList{s}
3. bs : |s| List
4. c : |s|
⊢ (c #∈ (as - bs)) > 0 ⇐⇒ ((c #∈ as) > 0) ∧ (¬((c #∈ bs) > 0))

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as:DisList\{s\}.  \mforall{}bs:|s|  List.  \mforall{}c:|s|.    c  \mmember{}\msubb{}  (as  -  bs)  =  (c  \mmember{}\msubb{}  as)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(c  \mmember{}\msubb{}  bs))


By

---

Latex:
((((RepD  THENM  BLemma  `iff\_imp\_equal\_bool`)  THENM  RW  bool\_to\_propC  0)
  THENM  RWH  (LemmaC  `mem\_iff\_count\_nzero`)  0
  )
  THENA  Auto
  )

---

Home Index