Theorem recseq

Description: Equality theorem for recs . (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Assertion	recseq	⊢ ( 𝐹 = 𝐺 → recs ( 𝐹 ) = recs ( 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		wrecseq3	⊢ ( 𝐹 = 𝐺 → wrecs ( E , On , 𝐹 ) = wrecs ( E , On , 𝐺 ) )
2		df-recs	⊢ recs ( 𝐹 ) = wrecs ( E , On , 𝐹 )
3		df-recs	⊢ recs ( 𝐺 ) = wrecs ( E , On , 𝐺 )
4	1 2 3	3eqtr4g	⊢ ( 𝐹 = 𝐺 → recs ( 𝐹 ) = recs ( 𝐺 ) )