---

Step * of Lemma test-exists-elim

∀[A:Type]. ∀[Q:A ⟶ A ⟶ ℙ].  ∀x,b:A.  (∃z:A × A. (Q[fst(z);snd(z)] ∧ (z = <x, b> ∈ (A × A))) ⇐⇒ Q[x;b] ∧ (x = x ∈ A))
BY
{ (UnivCD THENA Auto) }

1
1. [A] : Type
2. [Q] : A ⟶ A ⟶ ℙ
3. x : A
4. b : A
⊢ ∃z:A × A. (Q[fst(z);snd(z)] ∧ (z = <x, b> ∈ (A × A))) ⇐⇒ Q[x;b] ∧ (x = x ∈ A)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[Q:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x,b:A.    (\mexists{}z:A  \mtimes{}  A.  (Q[fst(z);snd(z)]  \mwedge{}  (z  =  <x,  b>))  \mLeftarrow{}{}\mRightarrow{}  Q[x;b]  \mwedge{}  (x  =  x))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index