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

Theorem leq 81
Description: Equality theorem for lambda abstraction.
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 38 . 2 |- = :((al -> be) -> ((al -> be) -> *))
2 leq.1 . . 3 |- A:be
32wl 59 . 2 |- \x:al A:(al -> be)
4 leq.2 . . . 4 |- R |= [A = B]
52, 4eqtypi 69 . . 3 |- B:be
65wl 59 . 2 |- \x:al B:(al -> be)
7 weq 38 . . . 4 |- = :(be -> (be -> *))
87, 2, 5, 4dfov1 66 . . 3 |- R |= (( = A)B)
92, 5, 8ax-leq 62 . 2 |- R |= (( = \x:al A)\x:al B)
101, 3, 6, 9dfov2 67 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 is referenced by:  hbxfrf  97  hbl  102  exval  133  euval  134  orval  137  anval  138  alrimiv  141  dfan2  144  olc  154  orc  155  exlimdv2  156  eta  166  cbvf  167  leqf  169  exlimd  171  ac  184  exmid  186  exnal  188  axpow  208  axun  209
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ceq 46  ax-leq 62
This theorem depends on definitions:  df-ov 65
  Copyright terms: Public domain W3C validator