---

Step * of Lemma l_all_single

∀[T:Type]. ∀t:T. ∀[P:{x:T| x = t ∈ T}  ⟶ ℙ]. ((∀x∈[t].P[x]) ⇐⇒ P[t])
BY
{ (RepUR ``l_all`` 0 THEN Auto THEN Reduce 0 THEN Auto) }

1
1. [T] : Type
2. t : T
3. [P] : {x:T| x = t ∈ T}  ⟶ ℙ
4. ∀i:ℕ1. P[[t][i]]
⊢ P[t]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}t:T.  \mforall{}[P:\{x:T|  x  =  t\}    {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x\mmember{}[t].P[x])  \mLeftarrow{}{}\mRightarrow{}  P[t])


By

---

Latex:
(RepUR  ``l\_all``  0  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index