Theorem wl 66

Description: The type of a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypothesis

Ref	Expression
wl.1	|- T:be

Assertion

Ref	Expression
wl	|- \x:al T:(al -> be)

Proof of Theorem wl

Step	Hyp	Ref	Expression
1		wl.1	. 2 |- T:be
2	1	ax-wl 65	1 |- \x:al T:(al -> be)

Syntax hints:   -> ht 2  \kl 6  wffMMJ2t 12

This theorem was proved from axioms:  ax-wl 65

This theorem is referenced by:  leq  91  beta  92  distrc  93  distrl  94  hbxfrf  107  hbc  110  hbl  112  clf  115  ovl  117  wal  134  wfal  135  wan  136  wim  137  wnot  138  wex  139  wor  140  weu  141  alval  142  exval  143  euval  144  orval  147  anval  148  ax4  150  alrimiv  151  cla4v  152  dfan2  154  olc  164  orc  165  exlimdv2  166  exlimdv  167  ax4e  168  cla4ev  169  19.8a  170  eta  178  cbvf  179  leqf  181  alrimi  182  exlimd  183  alimdv  184  eximdv  185  alnex  186  exnal1  187  ac  197  exmid  199  exnal  201  ax5  207  ax6  208  ax7  209  ax9  212  ax10  213  ax11  214  ax12  215  axext  219  axrep  220  axpow  221  axun  222