Theorem weqi 68

Description: Type of an equality.

Hypotheses

Ref	Expression
weqi.1	|- A:al
weqi.2	|- B:al

Assertion

Ref	Expression
weqi	|- [A = B]:*

Proof of Theorem weqi

Step	Hyp	Ref	Expression
1		weq 38	. 2 |- = :(al -> (al -> *))
2		weqi.1	. 2 |- A:al
3		weqi.2	. 2 |- B:al
4	1, 2, 3	wov 64	1 |- [A = B]:*

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

This theorem is referenced by:  clf  105  ovl  107  wal  124  wan  126  wim  127  weu  131  alval  132  exval  133  euval  134  notval  135  imval  136  orval  137  anval  138  pm2.21  143  dfan2  144  ecase  153  exlimdv2  156  exlimdv  157  ax4e  158  eta  166  cbvf  167  leqf  169  exlimd  171  ac  184  exmid  186  ax8  198  ax9  199  ax10  200  ax11  201  ax12  202  ax13  203  ax14  204  axext  206  axrep  207  axpow  208  axun  209