Theorem weqi 76

Description: Type of an equality. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
weqi.1	⊢ A:α
weqi.2	⊢ B:α

Assertion

Ref	Expression
weqi	⊢ [A = B]:∗

Proof of Theorem weqi

Step	Hyp	Ref	Expression
1		weq 41	. 2 ⊢ = :(α → (α → ∗))
2		weqi.1	. 2 ⊢ A:α
3		weqi.2	. 2 ⊢ B:α
4	1, 2, 3	wov 72	1 ⊢ [A = B]:∗

Syntax hints:  ∗hb 3   = ke 7  [kbr 9  wffMMJ2t 12

This theorem was proved from axioms:  ax-weq 40  ax-wov 71

This theorem is referenced by:  clf  115  ovl  117  wal  134  wan  136  wim  137  weu  141  alval  142  exval  143  euval  144  notval  145  imval  146  orval  147  anval  148  pm2.21  153  dfan2  154  ecase  163  exlimdv2  166  exlimdv  167  ax4e  168  eta  178  cbvf  179  leqf  181  exlimd  183  ac  197  exmid  199  ax8  211  ax9  212  ax10  213  ax11  214  ax12  215  ax13  216  ax14  217  axext  219  axrep  220  axpow  221  axun  222