---

Step * of Lemma quotient-bind-ext

∀A,B:Type. ∀a:⇃(A). ∀f:A ⟶ ⇃(B).  (f a ∈ ⇃(B))
BY
{ (UnivCD THENA Auto) }

1
1. A : Type
2. B : Type
3. a : ⇃(A)
4. f : A ⟶ ⇃(B)
⊢ f a ∈ ⇃(B)

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}a:\00D9(A).  \mforall{}f:A  {}\mrightarrow{}  \00D9(B).    (f  a  \mmember{}  \00D9(B))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index