Definition eqtypi 69

Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)

Hypotheses

Ref	Expression
eqcomi.1	⊢ A:α
eqcomi.2	⊢ R⊧[A = B]

Assertion

Ref	Expression
eqtypi	⊢ B:α

Detailed syntax breakdown of Definition eqtypi

Step	Hyp	Ref	Expression
1		hal	. 2 type α
2		tb	. 2 term B
3	1, 2	wffMMJ2t 12	1 wff B:α

This definition is referenced by:  eqcomi  70  mpbi  72  ceq12  78  leq  81  eqtri  85  3eqtr4i  86  3eqtr3i  87  oveq123  88  hbxfrf  97  clf  105  cl  106  cla4ev  159  cbvf  167  cbv  168  leqf  169  ac  184