Theorem rdgsuc

Description: The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

	Ref	Expression
Assertion	rdgsuc	|- ( B e. On -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		rdgfnon	|- rec ( F , A ) Fn On
2	1	fndmi	|- dom rec ( F , A ) = On
3	2	eleq2i	|- ( B e. dom rec ( F , A ) <-> B e. On )
4		rdgsucg	|- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
5	3 4	sylbir	|- ( B e. On -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )