---

Step * of Lemma bag-member-iff

∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;↓∃as:bag(T). (bs = ({x} + as) ∈ bag(T)))
BY
{ Auto }

1
1. T : Type
2. bs : bag(T)
3. x : T
4. x ↓∈ bs
⊢ ↓∃as:bag(T). (bs = ({x} + as) ∈ bag(T))

2
1. T : Type
2. bs : bag(T)
3. x : T
4. ↓∃as:bag(T). (bs = ({x} + as) ∈ bag(T))
⊢ x ↓∈ bs

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    uiff(x  \mdownarrow{}\mmember{}  bs;\mdownarrow{}\mexists{}as:bag(T).  (bs  =  (\{x\}  +  as)))


By

---

Latex:
Auto

---

Home Index