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

Theorem ceq2 90
Description: Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)
Hypotheses
Ref Expression
ceq12.1 |- F:(al -> be)
ceq12.2 |- A:al
ceq2.3 |- R |= [A = B]
Assertion
Ref Expression
ceq2 |- R |= [(FA) = (FB)]

Proof of Theorem ceq2
StepHypRef Expression
1 ceq12.1 . 2 |- F:(al -> be)
2 ceq12.2 . 2 |- A:al
3 ceq2.3 . . . 4 |- R |= [A = B]
43ax-cb1 29 . . 3 |- R:*
54, 1eqid 83 . 2 |- R |= [F = F]
61, 2, 5, 3ceq12 88 1 |- R |= [(FA) = (FB)]
Colors of variables: type var term
Syntax hints:   -> ht 2  kc 5   = 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-wov 71  ax-eqtypi 77
This theorem depends on definitions:  df-ov 73
This theorem is referenced by:  eqtri  95  clf  115  exval  143  euval  144  orval  147  exlimdv2  166  exlimdv  167  ax4e  168  cbvf  179  leqf  181  exlimd  183  ac  197  exmid  199  exnal  201  ax9  212  ax10  213  ax11  214  ax13  216  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator