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

Theorem leq 91
Description: Equality theorem for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
leq.1 |- A:be
leq.2 |- R |= [A = B]
Assertion
Ref Expression
leq |- R |= [\x:al A = \x:al B]
Distinct variable group:   x,R

Proof of Theorem leq
StepHypRef Expression
1 weq 41 . 2 |- = :((al -> be) -> ((al -> be) -> *))
2 leq.1 . . 3 |- A:be
32wl 66 . 2 |- \x:al A:(al -> be)
4 leq.2 . . . 4 |- R |= [A = B]
52, 4eqtypi 78 . . 3 |- B:be
65wl 66 . 2 |- \x:al B:(al -> be)
7 weq 41 . . . 4 |- = :(be -> (be -> *))
87, 2, 5, 4dfov1 74 . . 3 |- R |= (( = A)B)
92, 5, 8ax-leq 69 . 2 |- R |= (( = \x:al A)\x:al B)
101, 3, 6, 9dfov2 75 1 |- R |= [\x:al A = \x:al B]
Colors of variables: type var term
Syntax hints:   -> ht 2  \kl 6   = ke 7  [kbr 9   |= wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wl 65  ax-leq 69  ax-wov 71  ax-eqtypi 77
This theorem depends on definitions:  df-ov 73
This theorem is referenced by:  hbxfrf  107  hbl  112  exval  143  euval  144  orval  147  anval  148  alrimiv  151  dfan2  154  olc  164  orc  165  exlimdv2  166  eta  178  cbvf  179  leqf  181  exlimd  183  ac  197  exmid  199  exnal  201  axpow  221  axun  222
  Copyright terms: Public domain W3C validator