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

Theorem ceq2 80
Description: Equality theorem for combination.
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 73 . 2 |- R |= [F = F]
61, 2, 5, 3ceq12 78 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 is referenced by:  eqtri  85  clf  105  exval  133  euval  134  orval  137  exlimdv2  156  exlimdv  157  ax4e  158  cbvf  167  leqf  169  exlimd  171  ac  184  exmid  186  exnal  188  ax9  199  ax10  200  ax11  201  ax13  203  axrep  207  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
This theorem depends on definitions:  df-ov 65
  Copyright terms: Public domain W3C validator