---

Step * 1 of Lemma setmem-imageset


1. B : coSet{i:l}
2. f : coSet{i:l}
3. x : coSet{i:l}
⊢ (x ∈ B) ∧ ∃pr∈f.seteq(x;snd(pr)) ⇐⇒ (x ∈ B) ∧ (∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(x;snd(pr))))
BY
{ (RWO "existssetmem-iff" 0 THEN Auto THEN RWO  "-2" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  coSet\{i:l\}
2.  f  :  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
\mvdash{}  (x  \mmember{}  B)  \mwedge{}  \mexists{}pr\mmember{}f.seteq(x;snd(pr))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  B)  \mwedge{}  (\mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(x;snd(pr))))


By

---

Latex:
(RWO  "existssetmem-iff"  0  THEN  Auto  THEN  RWO    "-2"  (-1)  THEN  Auto)

---

Home Index