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

Axiom ax-leq 62
Description: Equality theorem for abstraction.
Hypotheses
Ref Expression
ax-leq.1 |- A:be
ax-leq.2 |- B:be
ax-leq.3 |- R |= (( = A)B)
Assertion
Ref Expression
ax-leq |- R |= (( = \x:al A)\x:al 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 al
4 vx . . . . 5 var x
5 ta . . . . 5 term A
63, 4, 5kl 6 . . . 4 term \x:al A
72, 6kc 5 . . 3 term ( = \x:al A)
8 tb . . . 4 term B
93, 4, 8kl 6 . . 3 term \x:al B
107, 9kc 5 . 2 term (( = \x:al A)\x:al B)
111, 10wffMMJ2 11 1 wff R |= (( = \x:al A)\x:al B)
Colors of variables: type var term
This axiom is referenced by:  leq  81
  Copyright terms: Public domain W3C validator