HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-beta GIF version

Axiom ax-beta 67
Description: Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypothesis
Ref Expression
ax-beta.1 A:β
Assertion
Ref Expression
ax-beta ⊤⊧(( = (λx:α Ax:α))A)

Detailed syntax breakdown of Axiom ax-beta
StepHypRef Expression
1 kt 8 . 2 term
2 ke 7 . . . 4 term =
3 hal . . . . . 6 type α
4 vx . . . . . 6 var x
5 ta . . . . . 6 term A
63, 4, 5kl 6 . . . . 5 term λx:α A
73, 4tv 1 . . . . 5 term x:α
86, 7kc 5 . . . 4 term (λx:α Ax:α)
92, 8kc 5 . . 3 term ( = (λx:α Ax:α))
109, 5kc 5 . 2 term (( = (λx:α Ax:α))A)
111, 10wffMMJ2 11 1 wff ⊤⊧(( = (λx:α Ax:α))A)
Colors of variables: type var term
This axiom is referenced by:  beta  92
  Copyright terms: Public domain W3C validator