---

Step * of Lemma ab_binrel_functionality

∀[T:Type]. ∀[E,E':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (E[x;y] ⇐⇒ E'[x;y])) ⇒ ((x,y:T. E[x;y]) <≡>{T} (x,y:T. E'[x;y])))
BY
{ ((RepD 
THENM Unfolds ``binrel_eqv ab_binrel`` 0 
THENM Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E,E':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:T.    (E[x;y]  \mLeftarrow{}{}\mRightarrow{}  E'[x;y]))  {}\mRightarrow{}  ((x,y:T.  E[x;y])  <\mequiv{}>\{T\}  (x,y:T.  E'[x;y])))


By

---

Latex:
((RepD 
THENM  Unfolds  ``binrel\_eqv  ab\_binrel``  0 
THENM  Reduce  0)  THEN  Auto)

---

Home Index