---

Step * of Lemma mem_iff_exists

∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (↑(a ∈b bs) ⇐⇒ ∃n:ℕ||bs||. (bs[n] = a ∈ |s|))
BY
{ ((UnivCD THENA Auto) THEN ((Unfold `mem` 0 THEN RWH (LemmaC `bexists_iff_exists_nth`) 0) THENA Auto')) }

1
1. s : DSet
2. a : |s|
3. bs : |s| List
⊢ ∃n:ℕ||bs||. (↑(bs[n] (=b) a)) ⇐⇒ ∃n:ℕ||bs||. (bs[n] = a ∈ |s|)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:|s|.  \mforall{}bs:|s|  List.    (\muparrow{}(a  \mmember{}\msubb{}  bs)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}||bs||.  (bs[n]  =  a))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ((Unfold  `mem`  0  THEN  RWH  (LemmaC  `bexists\_iff\_exists\_nth`)  0)  THENA  Auto')
  )

---

Home Index