---

Step * of Lemma equiv_rel_functionality_wrt_iff

∀[T,T':Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[E':T' ⟶ T' ⟶ ℙ].
  (∀x,y:T.  (E[x;y] ⇐⇒ E'[x;y])) ⇒ (EquivRel(T;x,y.E[x;y]) ⇐⇒ EquivRel(T';x,y.E'[x;y])) supposing T = T' ∈ Type
BY
{ (UnivCD THENA Auto) }

1
1. [T] : Type
2. [T'] : Type
3. [E] : T ⟶ T ⟶ ℙ
4. [E'] : T' ⟶ T' ⟶ ℙ
5. T = T' ∈ Type
6. ∀x,y:T.  (E[x;y] ⇐⇒ E'[x;y])@i
⊢ EquivRel(T;x,y.E[x;y]) ⇐⇒ EquivRel(T';x,y.E'[x;y])

---

Latex:

---

Latex:
\mforall{}[T,T':Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[E':T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}x,y:T.    (E[x;y]  \mLeftarrow{}{}\mRightarrow{}  E'[x;y]))  {}\mRightarrow{}  (EquivRel(T;x,y.E[x;y])  \mLeftarrow{}{}\mRightarrow{}  EquivRel(T';x,y.E'[x;y])) 
    supposing  T  =  T'


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index