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

Step	Hyp	Ref	Expression
1		ceq12.1	. 2 ⊢ F:(α → β)
2		ceq12.2	. 2 ⊢ A:α
3		ceq2.3	. . . 4 ⊢ R⊧[A = B]
4	3	ax-cb1 29	. . 3 ⊢ R:∗
5	4, 1	eqid 73	. 2 ⊢ R⊧[F = F]
6	1, 2, 5, 3	ceq12 78	1 ⊢ R⊧[(FA) = (FB)]

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