---

Step * 1 of Lemma member-fset-intersection


1. T : Type
2. eq : EqDecider(T)
3. a : fset(T)
4. b : fset(T)
5. x : T
⊢ uiff(x ∈ a ∧ x ∈ b;x ∈ a ∧ x ∈ b)
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  a  :  fset(T)
4.  b  :  fset(T)
5.  x  :  T
\mvdash{}  uiff(x  \mmember{}  a  \mwedge{}  x  \mmember{}  b;x  \mmember{}  a  \mwedge{}  x  \mmember{}  b)


By

---

Latex:
Auto

---

Home Index