Theorem weq 41

Description: The equality function has type al -> al -> *, i.e. it is polymorphic over all types, but the left and right type must agree. (Contributed by Mario Carneiro, 7-Oct-2014.)

Assertion

Ref	Expression
weq	|- = :(al -> (al -> *))

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		ax-weq 40	1 |- = :(al -> (al -> *))

Syntax hints:   -> ht 2  *hb 3   = ke 7  wffMMJ2t 12

This theorem was proved from axioms:  ax-weq 40

This theorem is referenced by:  wtru  43  eqcomx  52  weqi  76  eqcomi  79  mpbi  82  eqid  83  ded  84  ceq12  88  leq  91  beta  92  distrc  93  distrl  94  eqtri  95  oveq123  98  hbov  111  clf  115  ovl  117  alval  142  euval  144  imval  146  anval  148  eta  178  cbvf  179  leqf  181  ax10  213  axrep  220