Theorem rdgeq12

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

	Ref	Expression
Assertion	rdgeq12	$$⊢\left(F=G\wedge A=B\right)\to \mathrm{rec}\left(F,A\right)=\mathrm{rec}\left(G,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rdgeq2	$$⊢A=B\to \mathrm{rec}\left(F,A\right)=\mathrm{rec}\left(F,B\right)$$
2		rdgeq1	$$⊢F=G\to \mathrm{rec}\left(F,B\right)=\mathrm{rec}\left(G,B\right)$$
3	1 2	sylan9eqr	$$⊢\left(F=G\wedge A=B\right)\to \mathrm{rec}\left(F,A\right)=\mathrm{rec}\left(G,B\right)$$