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

Axiom ax-leq 69
Description: Equality theorem for abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
ax-leq.1 A:β
ax-leq.2 B:β
ax-leq.3 R⊧(( = A)B)
Assertion
Ref Expression
ax-leq R⊧(( = λx:α A)λx:α B)
Distinct variable group:   x,R

Detailed syntax breakdown of Axiom ax-leq
StepHypRef Expression
1 tr . 2 term R
2 ke 7 . . . 4 term =
3 hal . . . . 5 type α
4 vx . . . . 5 var x
5 ta . . . . 5 term A
63, 4, 5kl 6 . . . 4 term λx:α A
72, 6kc 5 . . 3 term ( = λx:α A)
8 tb . . . 4 term B
93, 4, 8kl 6 . . 3 term λx:α B
107, 9kc 5 . 2 term (( = λx:α A)λx:α B)
111, 10wffMMJ2 11 1 wff R⊧(( = λx:α A)λx:α B)
Colors of variables: type var term
This axiom is referenced by:  leq  91
  Copyright terms: Public domain W3C validator