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

Axiom ax-beta 67
Description: Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypothesis
Ref Expression
ax-beta.1 |- A:be
Assertion
Ref Expression
ax-beta |- T. |= (( = (\x:al Ax:al))A)

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