---

Step * 2 1 1 of Lemma set-elim

.....assertion..... 
1. A : Type
2. B : A ⟶ Type
3. a : A
4. a2 : B[a]
5. (λp.(fst(p))) <a, a2> ∈ A
⊢ ((λp.Ax) a2) = ((λp.Ax) a2) ∈ Image(B[fst(<a, a2>)],(λp.Ax))
BY
{ Refine_imageMemberEquality THEN Auto }

1
1. A : Type
2. B : A ⟶ Type
3. a : A
4. a2 : B[a]
5. (λp.(fst(p))) <a, a2> ∈ A
⊢ a2 ∈ B[fst(<a, a2>)]

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  a  :  A
4.  a2  :  B[a]
5.  (\mlambda{}p.(fst(p)))  <a,  a2>  \mmember{}  A
\mvdash{}  ((\mlambda{}p.Ax)  a2)  =  ((\mlambda{}p.Ax)  a2)


By

---

Latex:
Refine\_imageMemberEquality  THEN  Auto

---

Home Index