---

Step * 1 1 1 of Lemma quotient-bind-ext2


1. A : Type@i'
2. B : Type@i'
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)@i
10. f a ∈ ⇃(B)
11. f a1 ∈ ⇃(B)
⊢ (f a) = (f a1) ∈ ⇃(B)
BY
{ (BLemma `eq-in-quot` THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type@i'
2.  B  :  Type@i'
3.  a  :  Base
4.  a1  :  Base
5.  a  =  a1
6.  a  \mmember{}  A
7.  a1  \mmember{}  A
8.  True
9.  f  :  A  {}\mrightarrow{}  \00D9(B)@i
10.  f  a  \mmember{}  \00D9(B)
11.  f  a1  \mmember{}  \00D9(B)
\mvdash{}  (f  a)  =  (f  a1)


By

---

Latex:
(BLemma  `eq-in-quot`  THEN  Auto)

---

Home Index