---

Step * of Lemma isect_wf

∀[A:Type]. ∀[B:A ⟶ ℙ].  (⋂x:A. B[x] ∈ ℙ)
BY
{ (Fold `uall` 0 THEN Auto THEN (Unfold `member` 0 THEN UniverseInclusion 1)⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  \mBbbP{}].    (\mcap{}x:A.  B[x]  \mmember{}  \mBbbP{})


By

---

Latex:
(Fold  `uall`  0  THEN  Auto  THEN  (Unfold  `member`  0  THEN  UniverseInclusion  1)\mcdot{})

---

Home Index