---

Step * 1 1 of Lemma dset_set_wf


1. s : DSet
2. Q : |s| ⟶ ℙ
⊢ IsEqFun(|s|;=b)
BY
{ Unfold `eqfun_p` 0 THEN ((RepD) THENA Auto)  }

1
1. s : DSet
2. Q : |s| ⟶ ℙ
3. x : |s|
4. y : |s|
⊢ uiff(↑(x (=b) y);x = y ∈ |s|)

---

Latex:

---

Latex:

1.  s  :  DSet
2.  Q  :  |s|  {}\mrightarrow{}  \mBbbP{}
\mvdash{}  IsEqFun(|s|;=\msubb{})


By

---

Latex:
Unfold  `eqfun\_p`  0  THEN  ((RepD)  THENA  Auto) 

---

Home Index