---

Step * 1 of Lemma quotient-bind-ext


1. A : Type
2. B : Type
3. a : ⇃(A)
4. f : A ⟶ ⇃(B)
⊢ f a ∈ ⇃(B)
BY
{ DVar `a' }

1
1. A : Type
2. B : Type
3. a : Base
4. a1 : Base
5. a = a1 ∈ pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ True))
6. a ∈ A
7. a1 ∈ A
8. True
9. f : A ⟶ ⇃(B)
⊢ (f a) = (f a1) ∈ ⇃(B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  a  :  \00D9(A)
4.  f  :  A  {}\mrightarrow{}  \00D9(B)
\mvdash{}  f  a  \mmember{}  \00D9(B)


By

---

Latex:
DVar  `a'

---

Home Index