Theorem rdgsucmpt

Description: The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by Mario Carneiro, 9-Sep-2013)

	Ref	Expression
Hypotheses	rdgsucmpt.1	|- F = rec ( ( x e. _V |-> C ) , A )
	rdgsucmpt.2	|- ( x = ( F ` B ) -> C = D )
Assertion	rdgsucmpt	|- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )

Proof

Step	Hyp	Ref	Expression
1		rdgsucmpt.1	|- F = rec ( ( x e. _V |-> C ) , A )
2		rdgsucmpt.2	|- ( x = ( F ` B ) -> C = D )
3		nfcv	|- F/_ x A
4		nfcv	|- F/_ x B
5		nfcv	|- F/_ x D
6	3 4 5 1 2	rdgsucmptf	|- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )