This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rdgeq12

Description: Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion rdgeq12 ⊢ F = G ∧ A = B → rec ⁡ F A = rec ⁡ G B

Proof

Step Hyp Ref Expression
1 rdgeq2 ⊢ A = B → rec ⁡ F A = rec ⁡ F B
2 rdgeq1 ⊢ F = G → rec ⁡ F B = rec ⁡ G B
3 1 2 sylan9eqr ⊢ F = G ∧ A = B → rec ⁡ F A = rec ⁡ G B