---

Step * 2 1 of Lemma uimplies-iff-squash-implies

.....antecedent..... 
1. [P] : ℙ
2. [Q] : ℙ
3. [%1] : P
⊢ Image(P,(λx.Ax))
BY
{ UseWitness ⌜Ax⌝⋅ }

1
1. P : ℙ
2. Q : ℙ
3. P
⊢ Ax ∈ Image(P,(λx.Ax))

---

Latex:

---

Latex:
.....antecedent..... 
1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  [\%1]  :  P
\mvdash{}  Image(P,(\mlambda{}x.Ax))


By

---

Latex:
UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}

---

Home Index