---

Step * of Lemma subtype_rel_isect

∀[A,T:Type]. ∀[B:T ⟶ Type].  uiff(A ⊆r (⋂x:T. B[x]);∀[x:T]. (A ⊆r B[x]))
BY
{ Auto }

1
1. A : Type
2. T : Type
3. B : T ⟶ Type
4. A ⊆r (⋂x:T. B[x])
5. x : T
⊢ A ⊆r B[x]

---

Latex:

---

Latex:
\mforall{}[A,T:Type].  \mforall{}[B:T  {}\mrightarrow{}  Type].    uiff(A  \msubseteq{}r  (\mcap{}x:T.  B[x]);\mforall{}[x:T].  (A  \msubseteq{}r  B[x]))


By

---

Latex:
Auto

---

Home Index