---

Step * 2 of Lemma exists-pair


1. [A] : Type
2. [B] : Type
3. [P] : (A × B) ⟶ ℙ
4. a : A@i
5. b : B@i
6. P[<a, b>]@i
⊢ ∃p:A × B. P[p]
BY
{ (With ⌜<a, b>⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [P]  :  (A  \mtimes{}  B)  {}\mrightarrow{}  \mBbbP{}
4.  a  :  A@i
5.  b  :  B@i
6.  P[<a,  b>]@i
\mvdash{}  \mexists{}p:A  \mtimes{}  B.  P[p]


By

---

Latex:
(With  \mkleeneopen{}<a,  b>\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index