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