Definition wc 45

Description: The type of a combination.

Hypotheses

Ref	Expression
wc.1	⊢ F:(α → β)
wc.2	⊢ T:α

Assertion

Ref	Expression
wc	⊢ (FT):β

Detailed syntax breakdown of Definition wc

Step	Hyp	Ref	Expression
1		hbe	. 2 type β
2		tf	. . 3 term F
3		tt	. . 3 term T
4	2, 3	kc 5	. 2 term (FT)
5	1, 4	wffMMJ2t 12	1 wff (FT):β

This definition is referenced by:  eqcomx  47  ceq12  78  beta  82  distrc  83  distrl  84  eqtri  85  oveq123  88  hbxfrf  97  hbc  100  hbov  101  hbl  102  clf  105  ovl  107  wfal  125  wex  129  wor  130  weu  131  alval  132  exval  133  euval  134  notval  135  orval  137  ax4g  139  dfan2  144  notval2  149  notnot1  150  con3d  152  exlimdv2  156  exlimdv  157  ax4e  158  eta  166  cbvf  167  leqf  169  exlimd  171  alimdv  172  alnex  174  exnal1  175  ac  184  dfex2  185  exmid  186  notnot  187  exnal  188  ax3  192  ax5  194  ax6  195  ax7  196  ax9  199  ax10  200  ax11  201  ax12  202  ax13  203  ax14  204  axext  206  axrep  207  axpow  208  axun  209