Theorem ceq2 90

Description: Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

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 83	. 2 ⊢ R⊧[F = F]
6	1, 2, 5, 3	ceq12 88	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-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