---

Step * 1 of Lemma fset-intersection-commutes


1. A : Type
2. eqa : EqDecider(A)
3. x : fset(A)
4. y : fset(A)
⊢ ∀[a:A]. uiff(a ∈ x ⋂ y;a ∈ y ⋂ x)
BY
{ (Intro THEN ((RWO "member-fset-intersection" 0 THEN Auto) THEN D -1 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  eqa  :  EqDecider(A)
3.  x  :  fset(A)
4.  y  :  fset(A)
\mvdash{}  \mforall{}[a:A].  uiff(a  \mmember{}  x  \mcap{}  y;a  \mmember{}  y  \mcap{}  x)


By

---

Latex:
(Intro  THEN  ((RWO  "member-fset-intersection"  0  THEN  Auto)  THEN  D  -1  THEN  Auto)\mcdot{})

---

Home Index