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

Theorem ceq2 80
 Description: Equality theorem for combination.
Hypotheses
Ref Expression
ceq12.1 F:(αβ)
ceq12.2 A:α
ceq2.3 R⊧[A = B]
Assertion
Ref Expression
ceq2 R⊧[(FA) = (FB)]

Proof of Theorem ceq2
StepHypRef Expression
1 ceq12.1 . 2 F:(αβ)
2 ceq12.2 . 2 A:α
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 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 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
 Copyright terms: Public domain W3C validator