Theorem eqtypi 78

Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (Contributed by Mario Carneiro, 7-Oct-2014.)

Hypotheses

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

Assertion

Ref	Expression
eqtypi	⊢ B:α

Proof of Theorem eqtypi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ A:α
2		eqcomi.2	. 2 ⊢ R⊧[A = B]
3	1, 2	ax-eqtypi 77	1 ⊢ B:α

Syntax hints:   = ke 7  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-eqtypi 77

This theorem is referenced by:  eqcomi  79  mpbi  82  ceq12  88  leq  91  eqtri  95  3eqtr4i  96  3eqtr3i  97  oveq123  98  hbxfrf  107  clf  115  cl  116  cla4ev  169  cbvf  179  cbv  180  leqf  181  ac  197