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

Theorem leq 81
 Description: Equality theorem for lambda abstraction.
Hypotheses
Ref Expression
leq.1
leq.2
Assertion
Ref Expression
leq
Distinct variable group:   ,

Proof of Theorem leq
StepHypRef Expression
1 weq 38 . 2
2 leq.1 . . 3
32wl 59 . 2
4 leq.2 . . . 4
52, 4eqtypi 69 . . 3
65wl 59 . 2
7 weq 38 . . . 4
87, 2, 5, 4dfov1 66 . . 3
92, 5, 8ax-leq 62 . 2
101, 3, 6, 9dfov2 67 1
 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